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, 55 insertions, 14 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index f2aa4abad..454610b9b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -24,19 +24,60 @@ val check_connection : string list -> unit
 
 (** * The structure describing a coqtop sub-process *)
 
-type coqtop
+(** Liveness management of coqtop is automatic. Whenever a Coqtop dies abruptly,
+    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 
+    coqtop to close or to reset. *)
 
-(** * Count of all active coqtops *)
+type coqtop
+type handle
 
+(** Count of all active coqtops *)
 val coqtop_zombies : unit -> int
 
 (** * Starting / signaling / ending a real coqtop sub-process *)
 
-val spawn_coqtop : string list -> coqtop
-val respawn_coqtop : coqtop -> coqtop
-val kill_coqtop : coqtop -> unit
+(** 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
+
+(** Interrupt the current computation of coqtop. Asynchronous. *)
 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
+
+(** Last resort against a reluctant coqtop (a.k.a. chainsaw massacre). 
+    Asynchronous. *)
+val kill_coqtop : coqtop -> unit
+
+(** * Coqtop commmunication *)
+
+(** 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
+
+(** 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
+
+(** Check if coqtop is computing. Does not take any lock. *)
+val is_computing : coqtop -> bool
+
+(** Check if coqtop is closed. Does not take any lock. *)
+val is_closed : coqtop -> bool
+
 (** In win32, we'll use a different kill function than Unix.kill *)
 
 val killer : (int -> unit) ref
@@ -45,14 +86,14 @@ val interrupter : (int -> unit) ref
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
 val interp :
-  coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
-val rewind : coqtop -> int -> int Interface.value
-val status : coqtop -> Interface.status Interface.value
-val goals : coqtop -> Interface.goals option Interface.value
-val evars : coqtop -> Interface.evar list option Interface.value
-val hints : coqtop -> (Interface.hint list * Interface.hint) option Interface.value
-val inloadpath : coqtop -> string -> bool Interface.value
-val mkcases : coqtop -> string -> string list list Interface.value
+  handle -> ?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
 
 (** A specialized version of [raw_interp] dedicated to
     set/unset options. *)
@@ -68,5 +109,5 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> (t * bool) list -> unit
+  val set : handle -> (t * bool) list -> unit
 end