CoqIDE: pass the parent window to all methods liable to open a question box.

This is to ensure that the corresponding question boxes remains in
front of the main window, consistently with the fact that they are
blocking actions on the main window.

5 files changed, 51 insertions, 47 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 933ae322c7..f3e6731b38 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -181,8 +181,8 @@ let load_file ?(maycreate=false) f =
 let confirm_save ok =
   if ok then flash_info "Saved" else warning "Save Failed"
 
-let select_and_save ~saveas ?filename sn =
-  let do_save = if saveas then sn.fileops#saveas else sn.fileops#save in
+let select_and_save ?parent ~saveas ?filename sn =
+  let do_save = if saveas then sn.fileops#saveas ?parent else sn.fileops#save in
   let title = if saveas then "Save file as" else "Save file" in
   match select_file_for_save ~title ?filename () with
     |None -> false
@@ -192,9 +192,9 @@ let select_and_save ~saveas ?filename sn =
       if ok then sn.tab_label#set_text (Filename.basename f);
       ok
 
-let check_save ~saveas sn =
+let check_save ?parent ~saveas sn =
   try match sn.fileops#filename with
-    |None -> select_and_save ~saveas sn
+    |None -> select_and_save ?parent ~saveas sn
     |Some f ->
       let ok = sn.fileops#save f in
       confirm_save ok;
@@ -203,16 +203,17 @@ let check_save ~saveas sn =
 
 exception DontQuit
 
-let check_quit saveall =
+let check_quit ?parent saveall =
   (try save_pref () with _ -> flash_info "Cannot save preferences");
   let is_modified sn = sn.buffer#modified in
   if List.exists is_modified notebook#pages then begin
-    let answ = GToolbox.question_box ~title:"Quit"
+    let answ = Configwin_ihm.question_box ~title:"Quit"
       ~buttons:["Save Named Buffers and Quit";
                 "Quit without Saving";
                 "Don't Quit"]
       ~default:0
       ~icon:(warn_image ())#coerce
+      ?parent
       "There are unsaved buffers"
     in
     match answ with
@@ -269,15 +270,15 @@ let load _ =
     | None -> ()
     | Some f -> FileAux.load_file f
 
-let save _ = on_current_term (FileAux.check_save ~saveas:false)
+let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false)
 
-let saveas sn =
+let saveas ?parent sn =
   try
     let filename = sn.fileops#filename in
-    ignore (FileAux.select_and_save ~saveas:true ?filename sn)
+    ignore (FileAux.select_and_save ?parent ~saveas:true ?filename sn)
   with _ -> warning "Save Failed"
 
-let saveas = cb_on_current_term saveas
+let saveas ?parent = cb_on_current_term (saveas ?parent)
 
 let saveall _ =
   List.iter
@@ -288,33 +289,34 @@ let saveall _ =
 
 let () = Coq.save_all := saveall
 
-let revert_all _ =
+let revert_all ?parent _ =
   List.iter
-    (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)
+    (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert ?parent ())
     notebook#pages
 
-let quit _ =
-  try FileAux.check_quit saveall; exit 0
+let quit ?parent _ =
+  try FileAux.check_quit ?parent saveall; exit 0
   with FileAux.DontQuit -> ()
 
-let close_buffer sn =
+let close_buffer ?parent sn =
   let do_remove () = notebook#remove_page notebook#current_page in
   if not sn.buffer#modified then do_remove ()
   else
-    let answ = GToolbox.question_box ~title:"Close"
+    let answ = Configwin_ihm.question_box ~title:"Close"
       ~buttons:["Save Buffer and Close";
                 "Close without Saving";
                 "Don't Close"]
       ~default:0
       ~icon:(warn_image ())#coerce
+      ?parent
       "This buffer has unsaved modifications"
     in
     match answ with
-      | 1 when FileAux.check_save ~saveas:true sn -> do_remove ()
+      | 1 when FileAux.check_save ?parent ~saveas:true sn -> do_remove ()
       | 2 -> do_remove ()
       | _ -> ()
 
-let close_buffer = cb_on_current_term close_buffer
+let close_buffer ?parent = cb_on_current_term (close_buffer ?parent)
 
 let export kind sn =
   match sn.fileops#filename with
@@ -425,16 +427,16 @@ let coq_makefile sn =
 
 let coq_makefile = cb_on_current_term coq_makefile
 
-let editor sn =
+let editor ?parent sn =
   match sn.fileops#filename with
     |None -> warning "Call to external editor available only on named files"
     |Some f ->
       File.save ();
       let f = Filename.quote f in
       let cmd = Util.subst_command_placeholder cmd_editor#get f in
-      run_command ignore (fun _ -> sn.fileops#revert) cmd
+      run_command ignore (fun _ -> sn.fileops#revert ?parent ()) cmd
 
-let editor = cb_on_current_term editor
+let editor ?parent = cb_on_current_term (editor ?parent)
 
 let compile sn =
   File.save ();
@@ -936,7 +938,7 @@ let build_ui () =
     try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.coq_icon ())))
     with _ -> ()
   in
-  let _ = w#event#connect#delete ~callback:(fun _ -> File.quit (); true) in
+  let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in
   let _ = set_drag w#drag in
 
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
@@ -962,18 +964,18 @@ let build_ui () =
     item "File" ~label:"_File";
     item "New" ~callback:File.newfile ~stock:`NEW;
     item "Open" ~callback:File.load ~stock:`OPEN;
-    item "Save" ~callback:File.save ~stock:`SAVE ~tooltip:"Save current buffer";
-    item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:File.saveas;
+    item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
+    item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
     item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
     item "Revert all buffers" ~label:"_Revert all buffers"
-      ~callback:File.revert_all ~stock:`REVERT_TO_SAVED;
+      ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED;
     item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
-      ~callback:File.close_buffer ~tooltip:"Close current buffer";
+      ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer";
     item "Print..." ~label:"_Print..."
       ~callback:File.print ~stock:`PRINT ~accel:"<Ctrl>p";
     item "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l"
       ~callback:File.highlight ~stock:`REFRESH;
-    item "Quit" ~stock:`QUIT ~callback:File.quit;
+    item "Quit" ~stock:`QUIT ~callback:(File.quit ~parent:w);
   ];
 
   menu export_menu [
@@ -1005,7 +1007,7 @@ let build_ui () =
       ~accel:"<Shift>F3"
       ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
     item "External editor" ~label:"External editor" ~stock:`EDIT
-      ~callback:External.editor;
+      ~callback:(External.editor ~parent:w);
     item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
       ~callback:(fun _ ->
         begin
@@ -1298,8 +1300,8 @@ let build_ui () =
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
 
   (* Showtime ! *)
-  w#show ()
-
+  w#show ();
+  w
 
 
 (** {2 Coqide main function } *)
@@ -1314,7 +1316,7 @@ let make_scratch_buffer () =
   ()
 
 let main files =
-  build_ui ();
+  let w = build_ui () in
   reset_revert_timer ();
   reset_autosave_timer ();
   (match files with
@@ -1323,8 +1325,8 @@ let main files =
   notebook#goto_page 0;
   MiscMenu.initial_about ();
   on_current_term (fun t -> t.script#misc#grab_focus ());
-  Minilib.log "End of Coqide.main"
-
+  Minilib.log "End of Coqide.main";
+  w
 
 (** {2 Argument parsing } *)
 
@@ -1380,9 +1382,9 @@ let signals_to_crash =
   [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
    Sys.sigill; Sys.sigpipe; Sys.sigquit; Sys.sigusr1; Sys.sigusr2]
 
-let set_signal_handlers () =
+let set_signal_handlers ?parent () =
   try
-    Sys.set_signal Sys.sigint (Sys.Signal_handle File.quit);
+    Sys.set_signal Sys.sigint (Sys.Signal_handle (File.quit ?parent));
     List.iter
       (fun i -> Sys.set_signal i (Sys.Signal_handle FileAux.crash_save))
       signals_to_crash
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 03e8545377..1d438ec381 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -22,7 +22,7 @@ val logfile : string option ref
 val read_coqide_args : string list -> string list
 
 (** Prepare the widgets, load the given files in tabs *)
-val main : string list -> unit
+val main : string list -> GWindow.window
 
 (** Function to save anything and kill all coqtops
     @return [false] if you're allowed to quit. *)
@@ -37,7 +37,7 @@ val do_load : string -> unit
 
 (** Set coqide to perform a clean quit at Ctrl-C, while launching
     [crash_save] and exiting for others received signals *)
-val set_signal_handlers : unit -> unit
+val set_signal_handlers : ?parent:GWindow.window -> unit -> unit
 
 (** Emergency saving of opened files as "foo.v.crashcoqide",
     and exit (if the integer isn't 127). *)
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
index 91e8be875a..21f513b8f4 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide_main.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let _ = Coqide.set_signal_handlers ()
 let _ = GtkMain.Main.init ()
 
 (* We handle Gtk warning messages ourselves :
@@ -62,7 +61,8 @@ let () =
   let args = List.filter (fun x -> not (List.mem x files)) argl in
   Coq.check_connection args;
   Coqide.sup_args := args;
-  Coqide.main files;
+  let w = Coqide.main files in
+  Coqide.set_signal_handlers ~parent:w ();
   Coqide_os_specific.init ();
   try
     GMain.main ();
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index 7acd2c37a9..e4c8942cf1 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -18,10 +18,10 @@ object
   method filename : string option
   method update_stats : unit
   method changed_on_disk : bool
-  method revert : unit
+  method revert : ?parent:GWindow.window -> unit -> unit
   method auto_save : unit
   method save : string -> bool
-  method saveas : string -> bool
+  method saveas : ?parent:GWindow.window -> string -> bool
 end
 
 class fileops (buffer:GText.buffer) _fn (reset_handler:unit->unit) =
@@ -48,7 +48,7 @@ object(self)
           false
         |_ -> false
 
-  method revert =
+  method revert ?parent () =
     let do_revert f =
       push_info "Reverting buffer";
       try
@@ -72,13 +72,14 @@ object(self)
       | Some f ->
         if not buffer#modified then do_revert f
         else
-          let answ = GToolbox.question_box
+          let answ = Configwin_ihm.question_box
             ~title:"Modified buffer changed on disk"
             ~buttons:["Revert from File";
                       "Overwrite File";
                       "Disable Auto Revert"]
             ~default:0
             ~icon:(stock_to_widget `DIALOG_WARNING)
+            ?parent
             "Some unsaved buffers changed on disk"
           in
           match answ with
@@ -102,13 +103,14 @@ object(self)
     end
     else false
 
-  method saveas f =
+  method saveas ?parent f =
   if not (Sys.file_exists f) then self#save f
   else
-    let answ = GToolbox.question_box ~title:"File exists on disk"
+    let answ = Configwin_ihm.question_box ~title:"File exists on disk"
       ~buttons:["Overwrite"; "Cancel";]
       ~default:1
       ~icon:(warn_image ())#coerce
+      ?parent
       ("File "^f^" already exists")
     in
     match answ with
diff --git a/ide/fileOps.mli b/ide/fileOps.mli
index 9a1f0cb738..44a19f9981 100644
--- a/ide/fileOps.mli
+++ b/ide/fileOps.mli
@@ -16,10 +16,10 @@ object
   method filename : string option
   method update_stats : unit
   method changed_on_disk : bool
-  method revert : unit
+  method revert : ?parent:GWindow.window -> unit -> unit
   method auto_save : unit
   method save : string -> bool
-  method saveas : string -> bool
+  method saveas : ?parent:GWindow.window -> string -> bool
 end
 
 class fileops : GText.buffer -> string option -> (unit -> unit) -> ops