Coqide: get rid of threads, use gtk asynchronous i/o instead

 Threads were only there to handle blocking dialogs with the different
 coqtops. But programming with threads have drawbacks : complex mutex
 infrastructure, possible deadlocks, etc. In particular gtk functions
 are not meant to be called from a thread which isn't the gtk main loop,
 (unless some gtk mutex have been taken). This seem to pose problem
 specifically in win32 (and macosx ?), hence the use of the
 GtkThread.(a)sync hack for scheduling code for execution in the gtk
 main loop.

 Instead, we now use the Glib.Io module to install a callback that will
 be runned when some answer of coqtop is available on the channel.
 This implies using now a continuation-passing style: for instance,
 instead of two sequential requests to coqtop, we'll now have the
 2nd request inside the callback handling the answer to the 1st request.

 Remarks:

 - Also use asynchronous i/o for external commands (editor, coqc, make...).
   Launching an external editor or browser won't freeze coqide anymore.

 - Reworked handling of coqtop process, especially when closing them.
   A responsive coqtop should now hara-kiri immediatly when its input
   channel is closed. Otherwise we try later a soft kill, then some
   hard kills if necessary. If nothing work we warns the user.
   When quitting coqide, all this might induce a small delay (2s at worse).

 - Be careful now to avoid "long" computations (or blocking i/o) in
   a coqide function. Experimentally, it seems that loading/saving a .v
   file is quick enough. If necessary, we could use asynchronous i/o
   also for writing the .v, but for loading I've no clue.

 - In the Coqide module, we ensure that the current continuation k
   will indeed be run at the end thanks to an abstract return type
   (void = opaque copy of unit).

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

1 files changed, 16 insertions, 22 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 2e4ce364d..98ce63faf 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,18 +111,16 @@ object(self)
 	if String.get com (String.length com - 1) = '.'
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
-      let insert level message =
-        result#buffer#insert message;
-        result#buffer#insert "\n"
+      let log level message = result#buffer#insert (message^"\n")
       in
-      let process handle =
-        let answer = match Coq.interp handle insert ~raw:true phrase with
-        | Interface.Fail (l,str) ->
-            "Error while interpreting "^phrase^":\n"^str
-        | Interface.Good results | Interface.Unsafe results ->
-            "Result for command " ^ phrase ^ ":\n" ^ results
-        in
-        result#buffer#insert answer
+      let process h k =
+	Coq.interp ~logger:log ~raw:true phrase h (function
+          |Interface.Fail (l,str) ->
+            result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
+	    k ()
+          |Interface.Good res | Interface.Unsafe res ->
+            result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
+	    k ())
       in
       result#buffer#set_text "";
       Coq.try_grab coqtop process ignore
@@ -130,17 +128,13 @@ object(self)
     ignore (combo#entry#connect#activate ~callback:(on_activate callback));
     ignore (ok_b#connect#clicked ~callback:(on_activate callback));
 
-    begin match command,term with
-      | None,None -> ()
-      | Some c, None ->
-	  combo#entry#set_text c;
-
-      | Some c, Some t ->
-	  combo#entry#set_text c;
-	  entry#set_text t
-
-      | None , Some t ->
-	  entry#set_text t
+    begin match command with
+      | None -> ()
+      | Some c -> combo#entry#set_text c
+    end;
+    begin match term with
+      | None -> ()
+      | Some t -> entry#set_text t
     end;
     on_activate callback ();
     entry#misc#grab_focus ();