Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.

Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.

4 files changed, 8 insertions, 9 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 7edae47ca..1dd60ef02 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -232,7 +232,7 @@ type coqtop = {
   (* non quoted command-line arguments of coqtop *)
   mutable sup_args : string list;
   (* called whenever coqtop dies *)
-  mutable reset_handler : reset_kind -> unit task;
+  mutable reset_handler : unit task;
   (* called whenever coqtop sends a feedback message *)
   mutable feedback_handler : Feedback.feedback -> unit;
   (* actual coqtop process and its status *)
@@ -424,6 +424,7 @@ let mkready coqtop =
   fun () -> coqtop.status <- Ready; Void
 
 let rec respawn_coqtop ?(why=Unexpected) coqtop =
+  if why = Unexpected then warning "Coqtop died badly. Resetting.";
   clear_handle coqtop.handle;
   ignore_error (fun () ->
      coqtop.handle <-
@@ -435,7 +436,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
      If not, there isn't much we can do ... *)
   assert (coqtop.handle.alive = true);
   coqtop.status <- New;
-  ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
+  ignore (coqtop.reset_handler coqtop.handle (mkready coqtop))
 
 let spawn_coqtop sup_args =
   bind_self_as (fun this -> {
@@ -443,7 +444,7 @@ let spawn_coqtop sup_args =
                (fun () -> respawn_coqtop (this ()))
                (fun msg -> (this ()).feedback_handler msg);
     sup_args = sup_args;
-    reset_handler = (fun _ _ k -> k ());
+    reset_handler = (fun _ k -> k ());
     feedback_handler = (fun _ -> ());
     status = New;
   })
diff --git a/ide/coq.mli b/ide/coq.mli
index 7cef6a4d0..8a1fa3ed1 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -60,7 +60,7 @@ val is_computing : coqtop -> bool
 val spawn_coqtop : string list -> coqtop
 (** Create a coqtop process with some command-line arguments. *)
 
-val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
+val set_reset_handler : coqtop -> unit task -> unit
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 
 val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index f3ae317a3..80ce99a69 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -144,7 +144,7 @@ object
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
-  method handle_reset_initial : Coq.reset_kind -> unit task
+  method handle_reset_initial : unit task
   method raw_coq_query : string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
@@ -842,10 +842,8 @@ object(self)
     in
     loop l
 
-  method handle_reset_initial why =
+  method handle_reset_initial =
     let action () =
-      if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."
-      else
       (* clear the stack *)
       if Doc.focused document then Doc.unfocus document;
       while not (Doc.is_empty document) do
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 4a37a1fa5..332c18f2f 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,7 @@ object
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
-  method handle_reset_initial : Coq.reset_kind -> unit task
+  method handle_reset_initial : unit task
   method raw_coq_query : string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task