aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coq.ml13
-rw-r--r--ide/coq.mli1
-rw-r--r--ide/coqide.ml2
3 files changed, 15 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 0fe831ab3..42ab86dd6 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -410,8 +410,19 @@ let clear_handle h =
let mkready coqtop =
fun () -> coqtop.status <- Ready; Void
+let save_all = ref (fun () -> assert false)
+
let rec respawn_coqtop ?(why=Unexpected) coqtop =
- if why = Unexpected then warning "Coqtop died badly. Resetting.";
+ let () = match why with
+ | Unexpected ->
+ let title = "Warning" in
+ let icon = (warn_image ())#coerce in
+ let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in
+ let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in
+ if ans = 2 then (!save_all (); GtkMain.Main.quit ())
+ else if ans = 3 then GtkMain.Main.quit ()
+ | Planned -> ()
+ in
clear_handle coqtop.handle;
ignore_error (fun () ->
coqtop.handle <-
diff --git a/ide/coq.mli b/ide/coq.mli
index 5d9648603..463dd134a 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -170,3 +170,4 @@ val check_connection : string list -> unit
may terminate coqide in case of trouble *)
val interrupter : (int -> unit) ref
+val save_all : (unit -> unit) ref
diff --git a/ide/coqide.ml b/ide/coqide.ml
index feb45a7be..7b65c9fec 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -284,6 +284,8 @@ let saveall _ =
| Some f -> ignore (sn.fileops#save f))
notebook#pages
+let () = Coq.save_all := saveall
+
let revert_all _ =
List.iter
(fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)