From e17da6fc25eb7af0fbf59dfa6f1e3dd34c18edde Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Nov 2018 13:21:18 +0100 Subject: CoqIDE: Do not rebind up and down in microPG mode. First, they already work by default. Second, by rebinding them, they cannot be used any longer in the completion menu, which is a bit annoying. --- ide/nanoPG.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 002722ace9..f2913b1d1d 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -153,13 +153,13 @@ let emacs = insert emacs "Emacs" [] [ i#forward_sentence_end, { s with move = None })); mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> i#backward_sentence_start, { s with move = None })); - mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i -> + mkE _n "n" "Move to next line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#forward_line in let new_off = min (i#chars_in_line - 1) orig_off in (if new_off > 0 then i#set_line_offset new_off else i), { s with move = Some orig_off })); - mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i -> + mkE _p "p" "Move to previous line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#backward_line in let new_off = min (i#chars_in_line - 1) orig_off in -- cgit v1.2.3 From 3ccc9a89de9a2d5b81dae82c7815ba077f998135 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Nov 2018 13:22:43 +0100 Subject: CoqIDE: remove obselete menu item "Complete word". This was obsolete since new completion in 945d7db9 (then a07359f6). --- ide/coqide.ml | 2 -- ide/coqide_ui.ml | 1 - 2 files changed, 3 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 4190f43680..60ba9b5351 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1004,8 +1004,6 @@ let build_ui () = item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"F3" ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ())); - item "Complete Word" ~label:"Complete Word" ~accel:"slash" - ~callback:(fun _ -> ()); item "External editor" ~label:"External editor" ~stock:`EDIT ~callback:External.editor; item "Preferences" ~accel:"comma" ~stock:`PREFERENCES diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 91c529932f..c994898a4f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -60,7 +60,6 @@ let init () = \n \ \n \ \n \ -\n \ \n \ \n \ \n \ -- cgit v1.2.3 From 35a11a5567d660e545ad39c03b9bef39c26380ba Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Nov 2018 13:26:37 +0100 Subject: CoqIDE: ensure that the configuration box is not hidden by the main window. We do it by passing the name of the main window in the "parent" option. Formerly, the window could be hidden but nevertheless blocking any action on the main window. With the change, it can be moved aside, but never hidden by the main window. Tested on MacOS X. --- ide/configwin.ml | 4 ++-- ide/configwin.mli | 1 + ide/configwin_ihm.ml | 5 +++-- ide/configwin_ihm.mli | 1 + ide/coqide.ml | 2 +- ide/preferences.ml | 4 ++-- ide/preferences.mli | 2 +- 7 files changed, 11 insertions(+), 8 deletions(-) diff --git a/ide/configwin.ml b/ide/configwin.ml index 69e8b647ae..24be721631 100644 --- a/ide/configwin.ml +++ b/ide/configwin.ml @@ -46,6 +46,6 @@ let modifiers = Configwin_ihm.modifiers let edit ?(apply=(fun () -> ())) - title ?width ?height + title ?parent ?width ?height conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list + Configwin_ihm.edit ~with_apply: true ~apply title ?parent ?width ?height conf_struct_list diff --git a/ide/configwin.mli b/ide/configwin.mli index 7616e471db..0ee77d69b5 100644 --- a/ide/configwin.mli +++ b/ide/configwin.mli @@ -158,6 +158,7 @@ val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_ val edit : ?apply: (unit -> unit) -> string -> + ?parent:GWindow.window -> ?width:int -> ?height:int -> configuration_structure list -> diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml index d16efa603d..a6a3d52a38 100644 --- a/ide/configwin_ihm.ml +++ b/ide/configwin_ihm.ml @@ -662,12 +662,13 @@ class configuration_box (tt : GData.tooltips) conf_struct = to configure the various parameters. *) let edit ?(with_apply=true) ?(apply=(fun () -> ())) - title ?width ?height + title ?parent ?width ?height conf_struct = let dialog = GWindow.dialog ~position:`CENTER ~modal: true ~title: title - ?height ?width + ~type_hint:`DIALOG + ?parent ?height ?width () in let tooltips = GData.tooltips () in diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli index c867ad9127..94a3f12b39 100644 --- a/ide/configwin_ihm.mli +++ b/ide/configwin_ihm.mli @@ -60,6 +60,7 @@ val edit : ?with_apply:bool -> ?apply:(unit -> unit) -> string -> + ?parent:GWindow.window -> ?width:int -> ?height:int -> configuration_structure list -> diff --git a/ide/coqide.ml b/ide/coqide.ml index 60ba9b5351..933ae322c7 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1009,7 +1009,7 @@ let build_ui () = item "Preferences" ~accel:"comma" ~stock:`PREFERENCES ~callback:(fun _ -> begin - try Preferences.configure ~apply:refresh_notebook_pos () + try Preferences.configure ~apply:refresh_notebook_pos w with _ -> flash_info "Cannot save preferences" end; reset_revert_timer ()); diff --git a/ide/preferences.ml b/ide/preferences.ml index 6dc922c225..045d650c1c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -688,7 +688,7 @@ let pmodifiers ?(all = false) name p = modifiers name (str_to_mod_list p#get) -let configure ?(apply=(fun () -> ())) () = +let configure ?(apply=(fun () -> ())) parent = let cmd_coqtop = string ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s)) @@ -1068,7 +1068,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); *) - let x = edit ~apply "Customizations" cmds in + let x = edit ~apply "Customizations" ~parent cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); *) diff --git a/ide/preferences.mli b/ide/preferences.mli index dd2976efc2..7ed6a40bdb 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -107,7 +107,7 @@ val diffs : string preference val save_pref : unit -> unit val load_pref : unit -> unit -val configure : ?apply:(unit -> unit) -> unit -> unit +val configure : ?apply:(unit -> unit) -> GWindow.window -> unit val stick : 'a preference -> (#GObj.widget as 'obj) -> ('a -> unit) -> unit -- cgit v1.2.3 From 008354e71473ecdae0ca34dd5af951c4a4ae18dc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Nov 2018 15:05:58 +0100 Subject: A private copy of lablgtk's question_box supporting the "parent" option. The "parent" option allows to attach the box to the parent box. This ensures that the dialog box, which blocks action on the main window, does not get hidden by the main window. Idem for the message_box. --- ide/configwin_ihm.ml | 37 +++++++++++++++++++++++++++++++++++++ ide/configwin_ihm.mli | 9 +++++++++ 2 files changed, 46 insertions(+) diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml index a6a3d52a38..91695e944e 100644 --- a/ide/configwin_ihm.ml +++ b/ide/configwin_ihm.ml @@ -808,3 +808,40 @@ let custom ?label box f expand = custom_expand = expand ; custom_framed = label ; } + +(* Copying lablgtk question_box + forbidding hiding *) + +let question_box ~title ~buttons ?(default=1) ?icon ?parent message = + let button_nb = ref 0 in + let window = GWindow.dialog ~position:`CENTER ~modal:true ?parent ~type_hint:`DIALOG ~title () in + let hbox = GPack.hbox ~border_width:10 ~packing:window#vbox#add () in + let bbox = window#action_area in + begin match icon with + None -> () + | Some i -> hbox#pack i#coerce ~padding:4 + end; + ignore (GMisc.label ~text: message ~packing: hbox#add ()); + (* the function called to create each button by iterating *) + let rec iter_buttons n = function + [] -> + () + | button_label :: q -> + let b = GButton.button ~label: button_label + ~packing:(bbox#pack ~expand:true ~padding:4) () + in + ignore (b#connect#clicked ~callback: + (fun () -> button_nb := n; window#destroy ())); + (* If it's the first button then give it the focus *) + if n = default then b#grab_default () else (); + + iter_buttons (n+1) q + in + iter_buttons 1 buttons; + ignore (window#connect#destroy ~callback: GMain.Main.quit); + window#set_position `CENTER; + window#show (); + GMain.Main.main (); + !button_nb + +let message_box ~title ?icon ?parent ?(ok="Ok") message = + ignore (question_box ?icon ?parent ~title message ~buttons:[ ok ]) diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli index 94a3f12b39..772a0958ff 100644 --- a/ide/configwin_ihm.mli +++ b/ide/configwin_ihm.mli @@ -65,3 +65,12 @@ val edit : ?height:int -> configuration_structure list -> return_button + +val question_box : title:string -> + buttons:string list -> + ?default:int -> ?icon:#GObj.widget -> + ?parent:GWindow.window -> string -> int + +val message_box : + title:string -> ?icon:#GObj.widget -> + ?parent:GWindow.window -> ?ok:string -> string -> unit -- cgit v1.2.3 From a60461fdc0453a32451221d22e906ea74a0341e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Nov 2018 15:13:45 +0100 Subject: 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. --- ide/coqide.ml | 72 ++++++++++++++++++++++++++++-------------------------- ide/coqide.mli | 4 +-- ide/coqide_main.ml | 4 +-- ide/fileOps.ml | 14 ++++++----- ide/fileOps.mli | 4 +-- 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:"p"; item "Rehighlight" ~label:"Reh_ighlight" ~accel:"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:"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:"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 -- cgit v1.2.3