Heavily rewritten the coqtop management process of coqide. The coqtop

object is now responsible for restarting itself, and handles unexpected
crashes. Fixes a lot of errors in file descriptor management, but may
introduce lurking deadlocks and nasty bugs waiting to be discovered.

Only (quickly) tested under Linux, any callbacks from Windows are welcome.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 11 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index d52be74cb..e15e1960b 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,17 +111,14 @@ object(self)
 	if String.get com (String.length com - 1) = '.'
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
-      try
-        result#buffer#set_text
-          (match Coq.interp !coqtop ~raw:true phrase with
-             | Interface.Fail (l,str) ->
-                 ("Error while interpreting "^phrase^":\n"^str)
-             | Interface.Good results ->
-                 ("Result for command " ^ phrase ^ ":\n" ^ results))
-      with e ->
-	let s = Printexc.to_string e in
-	assert (Glib.Utf8.validate s);
-	result#buffer#set_text s
+      Coq.try_grab coqtop begin fun handle ->
+          result#buffer#set_text
+            (match Coq.interp handle ~raw:true phrase with
+              | Interface.Fail (l,str) ->
+                  ("Error while interpreting "^phrase^":\n"^str)
+              | Interface.Good results ->
+                  ("Result for command " ^ phrase ^ ":\n" ^ results))
+      end ignore
     in
     ignore (combo#entry#connect#activate ~callback:(on_activate callback));
     ignore (ok_b#connect#clicked ~callback:(on_activate callback));