diff options
| author | letouzey | 2011-03-28 09:54:30 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-28 09:54:30 +0000 |
| commit | 91e612f5705f22a8c9d8f04cc909db71b97850eb (patch) | |
| tree | 0d0ee599fb3f1fa257f95aea095b14b1f3d7f00c | |
| parent | f9d70b29cba88285ca08d12ac083be5455159330 (diff) | |
Ide: misc (nicer message than End_of_file, a useless try removed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 *) |