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

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);