diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-18 19:13:40 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-19 11:53:40 +0100 |
| commit | 37479c1b59b7492abb5c89a42c5a76d4cd9d48cd (patch) | |
| tree | 577e973a69941aef7ce20631dfbd74527a733815 /ide/coq.ml | |
| parent | 4f640bb24dfc45699670f41441355cdf71c83130 (diff) | |
CoqIDE: STOP button also stops workers (fix #4542)
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 15 |
1 files changed, 11 insertions, 4 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 |