diff options
| -rw-r--r-- | ide/coq.ml | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 9 |
2 files changed, 4 insertions, 8 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index cc41ee2304..89129b8c30 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -229,8 +229,7 @@ struct end let process_exn = function - | End_of_file -> - None, "Warning: End_of_file occurred (possibly a forced restart of coqtop)" + | End_of_file -> None, "Coqtop died" | e -> None, Printexc.to_string e let goals coqtop = diff --git a/ide/coqide.ml b/ide/coqide.ml index 1ce2133d1a..f40f27f433 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1002,12 +1002,9 @@ object(self) self#get_start_of_input end in - (try - while ((stop#compare (get_current())>=0) - && (self#process_next_phrase false false false)) - do () (* TODO: this looks obsolete : Util.check_for_interrupt ()*) done - with Sys.Break -> - prerr_endline "Interrupted during process_until_iter_or_error"); + while ((stop#compare (get_current())>=0) + && (self#process_next_phrase false false false)) + do () done; sync (fun _ -> self#show_goals; (* Start and stop might be invalid if an eol was added at eof *) |