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, 72 insertions, 50 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 43a040822..041485237 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -27,82 +27,104 @@ val check_connection : string list -> unit
 (** * The structure describing a coqtop sub-process *)
 
 (** Liveness management of coqtop is automatic. Whenever a Coqtop dies abruptly,
-    this module is responsible for relaunching the whole process. The hook 
+    this module is responsible for relaunching the whole process. The hook
     passed as an argument in coqtop construction will be called after such an
-    abrupt failure. In particular, it is NOT called when explicitely requesting 
+    abrupt failure. In particular, it is NOT called when explicitely requesting
     coqtop to close or to reset. *)
 
 type coqtop
 type handle
 
-(** Count of all active coqtops *)
-val coqtop_zombies : unit -> int
+(** * Coqtop tasks
+
+  A task is a group of sequential calls to be perform on a coqtop.
+  If a task is already sent to coqtop, it is considered busy
+  ([is_computing] will answer [true]), and other task submission
+  will be rejected.
+
+  A task is represented as a continuation, with a coqtop [handle]
+  as first argument, and a final inner continuation as 2nd argument.
+  This inner continuation should be runned at the end of the task.
+  Any exception occuring within the task will trigger a coqtop reset.
+*)
+
+type void
+type task = handle -> (unit->void) -> void
+
+(** Check if coqtop is computing, i.e. already has a current task *)
+val is_computing : coqtop -> bool
 
 (** * Starting / signaling / ending a real coqtop sub-process *)
 
-(** Create a coqtop process out of a hook and some command-line arguments.
-    The hook SHALL NOT use [grab] or its variants, otherwise you'll deadlock! *)
-val spawn_coqtop : (handle -> unit) -> string list -> coqtop
+(** Create a coqtop process with some command-line arguments. *)
+val spawn_coqtop : string list -> coqtop
 
-(** Interrupt the current computation of coqtop. Asynchronous. *)
+(** Register a handler called when a coqtop dies (badly or on purpose) *)
+type reset_kind = Planned | Unexpected
+val set_reset_handler : coqtop -> (reset_kind -> task) -> unit
+
+(** Finish initializing a freshly spawned coqtop, by running a first task on it.
+    The task should run its inner continuation at the end. *)
+val init_coqtop : coqtop -> task -> unit
+
+(** Interrupt the current computation of coqtop. *)
 val break_coqtop : coqtop -> unit
 
 (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
 val close_coqtop : coqtop -> unit
 
-(** Reset coqtop. Pending requests will be discarded. Default hook ignored, 
-    provided one used instead. *)
-val reset_coqtop : coqtop -> (handle -> unit) -> unit
+(** Reset coqtop. Pending requests will be discarded. The reset handler
+    of coqtop will be called with [Planned] as first argument *)
+val reset_coqtop : coqtop -> unit
 
-(** Last resort against a reluctant coqtop (a.k.a. chainsaw massacre). 
-    Asynchronous. *)
-val kill_coqtop : coqtop -> unit
+(** In win32, we'll use a different kill function than Unix.kill *)
 
-(** * Coqtop commmunication *)
+val killer : (int -> unit) ref
+val soft_killer : (int -> unit) ref
+val interrupter : (int -> unit) ref
 
-(** Start a coqtop dialogue and ensure that there is no interfering process.
-    - If coqtop ever dies during the computation, this function restarts coqtop 
-      and calls the restart hook with the fresh coqtop.
-    - If the argument function raises an exception, it is propagated.
-    - The request may be discarded if a [close_coqtop] or [reset_coqtop] occurs
-      before its completion.
-*)
-val grab : coqtop -> (handle -> unit) -> unit
+(** [set_final_countdown] triggers an exit of coqide after
+    some last cycles for closing remaining coqtop zombies *)
 
-(** As [grab], but applies the second callback if coqtop is already busy. Please
-    consider using [try_grab] instead of [grab] except if you REALLY want 
-    something to happen. *)
-val try_grab : coqtop -> (handle -> unit) -> (unit -> unit) -> unit
+val final_countdown : unit -> unit
 
-(** Check if coqtop is computing. Does not take any lock. *)
-val is_computing : coqtop -> bool
+(** * Coqtop commmunication *)
 
-(** Check if coqtop is closed. Does not take any lock. *)
-val is_closed : coqtop -> bool
+(** Try to schedule a task on a coqtop. If coqtop is available, the task
+    callback is run (asynchronously), otherwise the [(unit->unit)] callback
+    is triggered.
+    - If coqtop ever dies during the computation, this function restarts coqtop
+      and calls the restart hook with the fresh coqtop.
+    - If the argument function raises an exception, a coqtop reset occurs.
+    - The task may be discarded if a [close_coqtop] or [reset_coqtop] occurs
+      before its completion.
+    - The task callback should run its inner continuation at the end. *)
 
-(** In win32, we'll use a different kill function than Unix.kill *)
+val try_grab : coqtop -> task -> (unit -> unit) -> unit
 
-val killer : (int -> unit) ref
-val interrupter : (int -> unit) ref
+(** * Atomic calls to coqtop
 
-(** * Calls to Coqtop, cf [Serialize] for more details *)
+  These atomic calls can be combined to form arbitrary multi-call tasks.
+  They correspond to the protocol calls (cf [Serialize] for more details).
+  Note that each call is asynchronous: it will return immediately,
+  but the inner callback will be executed later to handle the call answer
+  when this answer is available.
+  Except for interp, we use the default logger for any call. *)
 
-type logger = Interface.message_level -> string -> unit
-(** Except for interp, we use the default logger for any call. *)
+type 'a atask = handle -> ('a Interface.value -> void) -> void
 
-val interp :
-  handle -> logger -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
-val rewind : handle -> int -> int Interface.value
-val status : handle -> Interface.status Interface.value
-val goals : handle -> Interface.goals option Interface.value
-val evars : handle -> Interface.evar list option Interface.value
-val hints : handle -> (Interface.hint list * Interface.hint) option Interface.value
-val inloadpath : handle -> string -> bool Interface.value
-val mkcases : handle -> string -> string list list Interface.value
-val search : handle -> Interface.search_flags -> string Interface.coq_object list Interface.value
+val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool ->
+  string -> string atask
+val rewind : int -> int atask
+val status : Interface.status atask
+val goals : Interface.goals option atask
+val evars : Interface.evar list option atask
+val hints : (Interface.hint list * Interface.hint) option atask
+val inloadpath : string -> bool atask
+val mkcases : string -> string list list atask
+val search : Interface.search_flags -> string Interface.coq_object list atask
 
-(** A specialized version of [raw_interp] dedicated to
-    set/unset options. *)
+(** A specialized version of [raw_interp] dedicated to set/unset options. *)
 
 module PrintOpt :
 sig
@@ -116,5 +138,5 @@ sig
   val universes : t
 
   val set_printing_width : int -> unit
-  val set : handle -> (t * bool) list -> unit
+  val set : (t * bool) list -> task
 end