From 91e612f5705f22a8c9d8f04cc909db71b97850eb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 28 Mar 2011 09:54:30 +0000
Subject: 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
---
 ide/coq.ml    | 3 +--
 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 *)
-- 
cgit v1.2.3