Robustness fix : clean restart of coqtop on pipe error + force matching

of coqtop return codes.

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

1 files changed, 10 insertions, 17 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 30ee75d417..4b59b5e75f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -27,7 +27,7 @@ val coqtop_zombies : unit -> int
 
 val reset_coqtop : coqtop -> unit
 
-exception Coq_failure of (Util.loc option * string)
+val process_exn : exn -> string*(Util.loc option)
 
 module PrintOpt :
 sig
@@ -40,32 +40,25 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> t -> bool -> unit
+  val set : coqtop -> t -> bool -> unit Ide_blob.value
 end
 
-val raw_interp : coqtop -> string -> unit
-
-val interp : coqtop -> bool -> string -> int
+val raw_interp : coqtop -> string -> unit Ide_blob.value
 
-val rewind : coqtop -> int -> int
+val interp : coqtop -> bool -> string -> int Ide_blob.value
 
-val read_stdout : coqtop -> string
-
-val process_exn : exn -> string*(Util.loc option)
+val rewind : coqtop -> int -> int Ide_blob.value
 
-val is_in_loadpath : coqtop -> string -> bool
+val read_stdout : coqtop -> string Ide_blob.value
 
-val make_cases : coqtop -> string -> string list list
+val is_in_loadpath : coqtop -> string -> bool Ide_blob.value
 
-type tried_tactic =
-  | Interrupted
-  | Success of int (* nb of goals after *)
-  | Failed
+val make_cases : coqtop -> string -> string list list Ide_blob.value
 
 (* Message to display in lower status bar. *)
 
-val current_status : coqtop -> string
+val current_status : coqtop -> string Ide_blob.value
 
-val goals : coqtop -> goals
+val goals : coqtop -> goals Ide_blob.value
 
 val msgnl : Pp.std_ppcmds -> string