aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:19:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:19:07 +0000
commit9555637d4b54e229e604db0bc8777564edd27691 (patch)
tree4e6c44eb707852e96969fb6d83069c86bdf55ba5
parent10d19da7aec5061cc19b09c06b619d10bda6b289 (diff)
Coqide: better handling of gtk messages + fix win32 stdout/stderr rerouting
We now try harder to handle ourselves gtk messages (e.g. Gtk-WARNING ...). This way, we could reroute them nicely in w32, and pop-up the critical ones. Moreover, the code rerouting debug messages to a log file in w32 was using !Ideutils.debug before its initialization. Now, when a log file is used, its name is displayed in the about messages. Btw, some code cleaning in coqide_main git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16037 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml10
-rw-r--r--ide/coqide.mli3
-rw-r--r--ide/coqide_main.ml4133
3 files changed, 103 insertions, 43 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b070f5df9..3001917bc 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -25,6 +25,8 @@ let autosave_timer = Ideutils.mktimer ()
let prefs = Preferences.current
+let logfile = ref None
+
class type _analyzed_view =
object
@@ -1578,6 +1580,12 @@ let detach_view _ =
(* If the buffer in the main window is closed, destroy this detached view *)
ignore (trm.script#connect#destroy ~callback:w#destroy)
+let log_file_message () =
+ if !Minilib.debug then
+ let file = match !logfile with None -> "stderr" | Some f -> f in
+ "\nDebug mode is on, log file is "^file
+ else ""
+
let initial_about () =
let initial_string =
"Welcome to CoqIDE, an Integrated Development Environment for Coq"
@@ -1588,7 +1596,7 @@ let initial_about () =
"\nYou are running " ^ coq_version
else ""
in
- let msg = initial_string ^ version_info in
+ let msg = initial_string ^ version_info ^ log_file_message () in
session_notebook#current_term.message_view#push Interface.Notice msg
let coq_icon () =
diff --git a/ide/coqide.mli b/ide/coqide.mli
index aba75be4b..ca5396950 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -12,6 +12,9 @@
no /bin/sh when using create_process instead of open_process. *)
val sup_args : string list ref
+(** In debug mode under win32, messages are written to a log file *)
+val logfile : string option ref
+
(** Filter the argv from coqide specific options, and set
Minilib.coqtop_path accordingly *)
val read_coqide_args : string list -> string list
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 3d14805eb..282dfce99 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -6,6 +6,53 @@
(* * 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). *)
@@ -20,12 +67,18 @@ let set_win32_path () =
*)
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 !Minilib.debug then
- Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log"))
+ 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
@@ -51,56 +104,52 @@ let () =
reroute_stdout_stderr ()
END
-let () =
- Coqide.set_signal_handlers ();
- ignore (GtkMain.Main.init ())
+(** MacOSX *)
IFDEF QUARTZ THEN
- let osx = GosxApplication.osxapplication ()
+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
- ()
+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 () =
- (* 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]);*)
- ignore (
- Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
- `WARNING;`CRITICAL]
- (fun ~level msg ->
- if level land Glib.Message.log_level `WARNING <> 0
- then Printf.eprintf "Warning: %s\n" msg
- else failwith ("Coqide internal error: " ^ msg)));
- let argl = Array.to_list Sys.argv in
+ 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 (List.tl argl) in
- let args = List.filter (fun x -> not (List.mem x files)) (List.tl 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 ())
-
-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
-
-let () =
+ 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);