blob: ebcecc172dc0043d4ae702292f725ac3262d542a (
plain)
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
136
137
138
139
140
141
142
143
144
145
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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 ()
(* 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, since coqide is now console-free, we re-route stdout/stderr
to avoid Sys_error if someone writes to them. We write to a pipe which
is never read (by default) or to a temp log file (when in debug mode).
*)
let reroute_stdout_stderr () =
(* We anticipate a bit the argument parsing and look for -debug *)
let debug = List.mem "-debug" (Array.to_list Sys.argv) in
Ideutils.debug := debug;
let out_descr =
if debug then
let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
Coqide.logfile := Some name;
Unix.descr_of_out_channel chan
else
snd (Unix.pipe ())
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. *)
(* Since [win32_interrupt] involves some hack about the process console,
only one should run at the same time, we simply skip execution of
[win32_interrupt] if another instance is already running *)
let ctrl_c_mtx = Mutex.create ()
let ctrl_c_protect f i =
if not (Mutex.try_lock ctrl_c_mtx) then ()
else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx
IFDEF WIN32 THEN
external win32_kill : int -> unit = "win32_kill"
external win32_interrupt : int -> unit = "win32_interrupt"
let () =
Coq.killer := win32_kill;
Coq.interrupter := ctrl_c_protect win32_interrupt;
set_win32_path ();
reroute_stdout_stderr ()
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
|
