CoqIDE: STOP button also stops workers (fix #4542)

5 files changed, 18 insertions, 7 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 98576a981..7edae47ca 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -465,10 +465,6 @@ let close_coqtop coqtop =
 
 let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop
 
-let break_coqtop coqtop =
-  try !interrupter (CoqTop.unixpid coqtop.handle.proc)
-  with _ -> Minilib.log "Error while sending Ctrl-C"
-
 let get_arguments coqtop = coqtop.sup_args
 
 let set_arguments coqtop args =
@@ -518,6 +514,17 @@ let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
 let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
 
+let break_coqtop coqtop workers =
+  if coqtop.status = Busy then
+    try !interrupter (CoqTop.unixpid coqtop.handle.proc)
+    with _ -> Minilib.log "Error while sending Ctrl-C"
+  else
+    let rec aux = function
+    | [] -> Void
+    | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws)
+    in
+      let Void = aux workers in ()
+
 module PrintOpt =
 struct
   type t = string list
diff --git a/ide/coq.mli b/ide/coq.mli
index d9eda0f34..7cef6a4d0 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
 
-val break_coqtop : coqtop -> unit
-(** Interrupt the current computation of coqtop. *)
+val break_coqtop : coqtop -> string list -> unit
+(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *)
 
 val close_coqtop : coqtop -> unit
 (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 608cf82ff..36aab30e6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -574,7 +574,7 @@ module Nav = struct
   let restart _ = on_current_term restart
   let interrupt sn =
     Minilib.log "User break received";
-    Coq.break_coqtop sn.coqtop
+    Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data))
   let interrupt = cb_on_current_term interrupt
   let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
diff --git a/ide/session.ml b/ide/session.ml
index 34c533b8e..168ddd4df 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -19,6 +19,7 @@ class type ['a] page =
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
     method refresh_color : unit -> unit
+    method data : 'a
   end
 
 class type control =
@@ -321,6 +322,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
       end
     method on_update ~callback:cb = callback := cb
     method refresh_color () = refresh ()
+    method data = !last_update
   end
 
 let create_jobpage coqtop coqops : jobpage =
@@ -361,6 +363,7 @@ let create_jobpage coqtop coqops : jobpage =
       end
     method on_update ~callback:cb = callback := cb
     method refresh_color () = refresh ()
+    method data = !last_update
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 0881e4039..ef39ab2e0 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -15,6 +15,7 @@ class type ['a] page =
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
     method refresh_color : unit -> unit
+    method data : 'a
   end
 
 class type control =