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/coqOps.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/coqOps.ml')
| -rw-r--r-- | ide/coqOps.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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 |