CoqIDE goes multiprocess

This commit changes many things in CoqIDE, and several breakage are to
be expected. So far, evaluation in standard tactic mode and backtracking
seems to be working.

Future work :
- clean up the thread management crud remaining in ide/coqide.ml
- rework the exception handling
- rework the init system in Coqtop

plus many other things

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

3 files changed, 37 insertions, 7 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74c4ff3db..440d36280 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -150,6 +150,7 @@ let usage () =
 
 let warning s = msg_warning (str s)
 
+let ide_slave = ref false
 
 let ide_args = ref []
 let parse_args arglist =
@@ -287,6 +288,8 @@ let parse_args arglist =
 
     | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
 
+    | "-ideslave" :: rem -> ide_slave := true; parse rem
+
     | s :: rem ->
 	  ide_args := s :: !ide_args;
 	  parse rem
@@ -308,6 +311,12 @@ let init arglist =
   begin
     try
       parse_args arglist;
+      if !ide_args <> [] then usage ();
+      if !ide_slave then begin
+        Flags.make_silent true;
+        Pfedit.set_undo (Some 5000);
+        Ide_blob.init_stdout ()
+      end;
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
@@ -342,13 +351,14 @@ let init_ide arglist =
   Flags.make_silent true;
   Pfedit.set_undo (Some 5000);
   Ide_blob.init_stdout ();
-  init arglist;
   List.rev !ide_args
 
 let start () =
   init_toplevel (List.tl (Array.to_list Sys.argv));
-  if !ide_args <> [] then usage ();
-  Toplevel.loop();
+  if !ide_slave then
+    Ide_blob.loop ()
+  else
+    Toplevel.loop();
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index a312b0037..899cee1e4 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -403,7 +403,9 @@ let concl_next_tac sigma concl =
   ])
 
 let current_goals () =
-  let pfts = Pfedit.get_pftreestate () in
+  let pfts =
+    Proof_global.give_me_the_proof ()
+  in
   let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
   if all_goals = [] then
     begin
@@ -524,12 +526,14 @@ type 'a call =
 
 type 'a value =
   | Good of 'a
-  | Fail of exn
+  | Fail of (Util.loc * Pp.std_ppcmds)
 
 let eval_call c = 
+  let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
   let filter_compat_exn = function
     | Vernac.DuringCommandInterp (loc,inner)
     | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner
+    | Vernacexpr.Quit -> raise Vernacexpr.Quit
     | e -> e
   in
   try Good (match c with
@@ -541,7 +545,11 @@ let eval_call c =
               | Cur_goals -> Obj.magic (current_goals ())
               | Cur_status -> Obj.magic (current_status ())
               | Cases s -> Obj.magic (make_cases s))
-  with e -> Fail (filter_compat_exn e)
+  with e ->
+    let (l,pp) = explain_exn (filter_compat_exn e) in
+    (* force evaluation of format stream *)
+    Pp.msg_with null_formatter pp;
+    Fail (l,pp)
 
 let is_in_loadpath s : bool call =
   In_loadpath s
@@ -568,3 +576,14 @@ let make_cases s : string list list call =
   Cases s
 
 (* End of wrappers *)
+
+let loop () =
+  try
+    while true do
+      let q = (Safe_marshal.receive: in_channel -> 'a call) stdin in
+      let r = eval_call q in
+      Safe_marshal.send stdout r
+    done
+  with
+    | Vernacexpr.Quit -> exit 0
+    | _ -> exit 1
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
index c74d67f2c..561821b56 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_blob.mli
@@ -23,7 +23,7 @@ type 'a call
 
 type 'a value =
   | Good of 'a
-  | Fail of exn
+  | Fail of (Util.loc * Pp.std_ppcmds)
 
 val eval_call : 'a call -> 'a value
 
@@ -43,3 +43,4 @@ val current_goals : goals call
 
 val read_stdout : string call
 
+val loop : unit -> unit