1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
let _ = Coqide.ignore_break ()
let _ = GtkMain.Main.init ()
(* We handle Gtk warning messages ourselves :
- on win32, we don't want them to end on a non-existing console
- we display critical messages via pop-ups *)
let catch_gtk_messages () =
let all_levels =
[`FLAG_RECURSION;`FLAG_FATAL;`ERROR;`CRITICAL;`WARNING;
`MESSAGE;`INFO;`DEBUG]
in
let handler ~level msg =
let header = "Coqide internal error: " in
let level_is tag = (level land Glib.Message.log_level tag) <> 0 in
if level_is `ERROR then
let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
Coqide.crash_save 1
else if level_is `CRITICAL then
GToolbox.message_box ~title:"Error" (header ^ msg)
else if level_is `DEBUG || Sys.os_type = "Win32" then
Ideutils.prerr_endline msg (* no-op unless in debug mode *)
else
Printf.eprintf "%s\n" msg
in
let catch domain =
ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler)
in
List.iter catch ["GLib";"Gtk";"Gdk";"Pango"]
let () = catch_gtk_messages ()
(* We anticipate a bit the argument parsing and look for -debug *)
let early_set_debug () =
Ideutils.debug := List.mem "-debug" (Array.to_list Sys.argv)
(* On win32, we add the directory of coqide to the PATH at launch-time
(this used to be done in a .bat script). *)
let set_win32_path () =
Unix.putenv "PATH"
(Filename.dirname Sys.executable_name ^ ";" ^
(try Sys.getenv "PATH" with _ -> ""))
(* On win32, in debug mode we duplicate stdout/stderr in a log file. *)
let log_stdout_stderr () =
let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
Coqide.logfile := Some name;
let out_descr = Unix.descr_of_out_channel chan in
Unix.set_close_on_exec out_descr;
Unix.dup2 out_descr Unix.stdout;
Unix.dup2 out_descr Unix.stderr
(* We also provide specific kill and interrupt functions. *)
IFDEF WIN32 THEN
external win32_kill : int -> unit = "win32_kill"
external win32_interrupt_all : unit -> unit = "win32_interrupt_all"
external win32_hide_console : unit -> unit = "win32_hide_console"
let () =
set_win32_path ();
Coq.killer := win32_kill;
Coq.interrupter := (fun pid -> win32_interrupt_all ());
early_set_debug ();
if !Ideutils.debug then
log_stdout_stderr ()
else
win32_hide_console ()
END
IFDEF QUARTZ THEN
let osx = GosxApplication.osxapplication ()
let _ =
osx#connect#ns_application_open_file ~callback:(fun x -> Coqide.do_load x; true) in
let _ =
osx#connect#ns_application_block_termination ~callback:Coqide.forbid_quit_to_save in
()
END
let () =
(try
let gtkrcdir = List.find
(fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc"))
Minilib.xdg_config_dirs in
GtkMain.Rc.add_default_file (Filename.concat gtkrcdir "coqide-gtk2rc");
with Not_found -> ());
(* Statup preferences *)
begin
try Preferences.load_pref ()
with e ->
Ideutils.flash_info ("Could not load preferences ("^Printexc.to_string e^").");
end;
(* GtkData.AccelGroup.set_default_mod_mask
(Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*)
let argl = Array.to_list Sys.argv in
let argl = Coqide.read_coqide_args argl in
let files = Coq.filter_coq_opts (List.tl argl) in
let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
Coq.check_connection args;
Coqide.sup_args := args;
Coqide.main files;
if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ())
IFDEF QUARTZ THEN
let () =
GtkosxApplication.Application.set_menu_bar osx#as_osxapplication (GtkMenu.MenuShell.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) in
let () =
GtkosxApplication.Application.insert_app_menu_item osx#as_osxapplication (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 in
let () =
GtkosxApplication.Application.set_help_menu osx#as_osxapplication (Some (GtkMenu.MenuItem.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) in
osx#ready ()
END
while true do
try
GtkThread.main ()
with
| Sys.Break -> Ideutils.prerr_endline "Interrupted."
| e ->
Minilib.safe_prerr_endline
("CoqIde unexpected error:" ^ (Printexc.to_string e));
Coqide.crash_save 127
done
|