aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/configwin.ml4
-rw-r--r--ide/configwin.mli1
-rw-r--r--ide/configwin_ihm.ml42
-rw-r--r--ide/configwin_ihm.mli10
-rw-r--r--ide/coqide.ml76
-rw-r--r--ide/coqide.mli4
-rw-r--r--ide/coqide_main.ml4
-rw-r--r--ide/coqide_ui.ml1
-rw-r--r--ide/fileOps.ml14
-rw-r--r--ide/fileOps.mli4
-rw-r--r--ide/nanoPG.ml4
-rw-r--r--ide/preferences.ml4
-rw-r--r--ide/preferences.mli2
13 files changed, 110 insertions, 60 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..91695e944e 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
@@ -807,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 c867ad9127..772a0958ff 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
@@ -60,7 +60,17 @@ val edit :
?with_apply:bool ->
?apply:(unit -> unit) ->
string ->
+ ?parent:GWindow.window ->
?width:int ->
?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
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a26f7d1b94..75b0fd7455 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -190,8 +190,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
@@ -201,9 +201,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;
@@ -212,16 +212,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
@@ -278,15 +279,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
@@ -297,33 +298,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
@@ -434,16 +436,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 ();
@@ -945,7 +947,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
@@ -971,18 +973,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 [
@@ -1013,14 +1015,12 @@ let build_ui () =
item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
~accel:"<Shift>F3"
~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
- item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
- ~callback:(fun _ -> ());
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
- 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 ());
@@ -1309,8 +1309,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 } *)
@@ -1325,7 +1325,7 @@ let make_scratch_buffer () =
()
let main files =
- build_ui ();
+ let w = build_ui () in
reset_revert_timer ();
reset_autosave_timer ();
(match files with
@@ -1334,8 +1334,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 } *)
@@ -1391,9 +1391,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/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 <menuitem action='Find' />\
\n <menuitem action='Find Next' />\
\n <menuitem action='Find Previous' />\
-\n <menuitem action='Complete Word' />\
\n <separator />\
\n <menuitem action='External editor' />\
\n <separator />\
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
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:16:34 +0000