blob: 282dfce998920e1aff1e46b58345164c7964e96c (
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
146
147
148
149
150
151
152
153
154
155
156
|
(************************************************************************)
(* 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.set_signal_handlers ()
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 log_level lvl =
let level_is tag = (lvl land Glib.Message.log_level tag) <> 0 in
if level_is `ERROR then `FATAL
else if level_is `CRITICAL then `ERROR
else if level_is `DEBUG then `DEBUG
else if level_is `WARNING then `WARNING
else if level_is `MESSAGE then `NOTICE
else `INFO
in
let handler ~level msg =
let header = "Coqide internal error: " in
match log_level level with
|`FATAL ->
let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
Coqide.crash_save 1
|`ERROR -> GToolbox.message_box ~title:"Error" (header ^ msg)
|`DEBUG -> Minilib.log msg
|level when Sys.os_type = "Win32" -> Minilib.log ~level msg
|_ -> 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 ()
(** System-dependent settings *)
let os_specific_init () = ()
(** Win32 *)
(* 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
Minilib.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
(** MacOSX *)
IFDEF QUARTZ THEN
let osx = GosxApplication.osxapplication ()
let () =
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 ()
let os_specific_init () =
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
let load_prefs () =
try Preferences.load_pref ()
with e -> Ideutils.flash_info
("Could not load preferences ("^Printexc.to_string e^").")
let () =
load_prefs ();
let argl = List.tl (Array.to_list Sys.argv) in
let argl = Coqide.read_coqide_args argl in
let files = Coq.filter_coq_opts argl in
let args = List.filter (fun x -> not (List.mem x files)) 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 ());
os_specific_init ();
try GtkThread.main ()
with e ->
Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e);
Coqide.crash_save 127
|
