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, 5 insertions, 1 deletions

diff --git a/ide/coqide.mli b/ide/coqide.mli
index ca5396950..f9e711455 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -24,7 +24,11 @@ val main : string list -> unit
 
 (** Function to save anything and kill all coqtops
     @return [false] if you're allowed to quit. *)
-val forbid_quit_to_save : unit -> bool
+val forbid_quit : unit -> bool
+
+(** Terminate coqide after closing all coqtops and waiting
+    for their death *)
+val close_and_quit : unit -> unit
 
 (** Function to load of a file. *)
 val do_load : string -> unit