diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 00:16:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 00:23:00 +0200 |
| commit | 47098e8619f269ddaaf621936ae90b9dfa128871 (patch) | |
| tree | 9f538f6801e506d7eea5d01d3b80d1396a47e808 /ide/coq.ml | |
| parent | 4b4397e185cee54052819ad63bef3ecd56ba4512 (diff) | |
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.
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 7 |
1 files changed, 4 insertions, 3 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; }) |