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

11 files changed, 158 insertions, 70 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index beb8ebb526..1b768de9a2 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+let get_current_toplevel = ref (fun () -> Coq.dummy_coqtop)
+
 class command_window () =
 (*  let window = GWindow.window
 		 ~allow_grow:true ~allow_shrink:true
@@ -104,9 +106,10 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	Coq.raw_interp Coq.dummy_coqtop phrase;
+        let curtop = !get_current_toplevel () in
+	Coq.raw_interp curtop phrase;
 	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop))
+	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout curtop))
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index b211afabdc..24e79cb933 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -17,4 +17,4 @@ class command_window :
 
 val command_window : unit -> command_window
 
-
+val get_current_toplevel : (unit -> Coq.coqtop) ref
diff --git a/ide/coq.ml b/ide/coq.ml
index f385ae0489..fecd3f2922 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -47,9 +47,8 @@ let msg m =
 let msgnl m =
   (msg m)^"\n"
 
-let init () =
-  Coqtop.init_ide (List.tl (Array.to_list Sys.argv))
-
+let init () = List.tl (Array.to_list Sys.argv)
+(*  Coqtop.init_ide (List.tl (Array.to_list Sys.argv))*)
 
 let i = ref 0
 
@@ -83,22 +82,40 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let eval_call c =
-  match Ide_blob.eval_call c with
+exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+
+let eval_call coqtop (c:'a Ide_blob.call) =
+  Safe_marshal.send coqtop.cin c;
+  let res = (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout in
+  match res with
     | Ide_blob.Good v -> v
-    | Ide_blob.Fail e -> raise e
+    | Ide_blob.Fail (l,pp) -> prerr_endline (msg pp); raise (Coq_failure (l,pp))
 
-let is_in_loadpath coqtop s = eval_call (Ide_blob.is_in_loadpath s)
+let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
  
 let reset_initial = Ide_blob.reinit
 
-let raw_interp coqtop s = eval_call (Ide_blob.raw_interp s)
+let raw_interp coqtop s = eval_call coqtop (Ide_blob.raw_interp s)
 
-let interp coqtop b s = eval_call (Ide_blob.interp b s)
+let interp coqtop b s = eval_call coqtop (Ide_blob.interp b s)
 
-let rewind coqtop i = eval_call (Ide_blob.rewind i)
+let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i)
  
-let read_stdout coqtop = eval_call Ide_blob.read_stdout
+let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout
+
+let spawn_coqtop () =
+  let prog = Sys.argv.(0) in
+  let dir = Filename.dirname prog in
+  let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave") in
+  { cin = ic; cout = oc }
+
+let kill_coqtop coqtop = raw_interp coqtop "Quit."
+
+let reset_coqtop coqtop =
+  kill_coqtop coqtop;
+  let ni = spawn_coqtop () in
+  coqtop.cin <- ni.cin;
+  coqtop.cout <- ni.cout
 
 module PrintOpt =
 struct
@@ -120,10 +137,10 @@ struct
     List.iter
       (fun cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         raw_interp dummy_coqtop str)
+         raw_interp coqtop str)
       opt
 
-  let enforce_hack () = Hashtbl.iter (set ()) state_hack 
+  let enforce_hack coqtop = Hashtbl.iter (set coqtop) state_hack 
 end
 
 let rec is_pervasive_exn = function
@@ -158,15 +175,15 @@ let print_toplevel_error exc =
 
 let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
-type  tried_tactic =
+type tried_tactic =
   | Interrupted
   | Success of int (* nb of goals after *)
   | Failed
 
 let goals coqtop =
-  PrintOpt.enforce_hack ();
-  eval_call Ide_blob.current_goals
+  PrintOpt.enforce_hack coqtop;
+  eval_call coqtop Ide_blob.current_goals
 
-let make_cases coqtop s = eval_call (Ide_blob.make_cases s)
+let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
 
-let current_status coqtop = eval_call Ide_blob.current_status
+let current_status coqtop = eval_call coqtop Ide_blob.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index d50aab2802..914eb708a5 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -19,6 +19,14 @@ type coqtop
 
 val dummy_coqtop : coqtop
 
+val spawn_coqtop : unit -> coqtop
+
+val kill_coqtop : coqtop -> unit
+
+val reset_coqtop : coqtop -> unit
+
+exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+
 module PrintOpt :
 sig
   type t
@@ -61,3 +69,5 @@ type tried_tactic =
 val current_status : coqtop -> string
 
 val goals : coqtop -> goals
+
+val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e8e4252780..e8198ec6fe 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -101,6 +101,7 @@ type viewable_script =
      proof_view : GText.view;
      message_view : GText.view;
      analyzed_view : analyzed_views;
+     toplvl : Coq.coqtop;
     }
 
 
@@ -181,7 +182,7 @@ let set_active_view i =
   prerr_endline "entering set_active_view";
   (try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ());
   session_notebook#goto_page i;
-  let s = session_notebook#current_term in
+  let s = session_notebook#get_nth_term i in
     s.tab_label#set_use_markup true;
     s.tab_label#set_label ("<span background=\"light green\">"^s.tab_label#text^"</span>");
     active_view := i;
@@ -279,6 +280,7 @@ let kill_input_view i =
     v.tab_label#destroy ();
     v.proof_view#destroy ();
     v.message_view#destroy ();
+    Coq.kill_coqtop v.toplvl;
     session_notebook#remove_page i
 (*
 (* XXX - beaucoups d'appels, a garder *)
@@ -289,6 +291,19 @@ let remove_current_view_page () =
   let c = session_notebook#current_page in
     kill_input_view c
 
+let print_items = [
+  ([implicit],"Display _implicit arguments",GdkKeysyms._i,false);
+  ([coercions],"Display _coercions",GdkKeysyms._c,false);
+  ([raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
+  ([notations],"Display _notations",GdkKeysyms._n,true);
+  ([all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
+  ([existential],"Display _existential variable instances",GdkKeysyms._e,false);
+  ([universes],"Display _universe levels",GdkKeysyms._u,false);
+  ([all_basic;existential;universes],"Display all _low-level contents",GdkKeysyms._l,false)
+]
+
+let setopts ct opts v =
+  List.iter (fun o -> set ct o v) opts
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -375,9 +390,9 @@ exception Stop of int
 (* XXX *)
 let activate_input i =
   prerr_endline "entering activate_input";
-  (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
+(*  (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
    with _ -> ());
-  (session_notebook#get_nth_term i).analyzed_view#activate ();
+  (session_notebook#get_nth_term i).analyzed_view#activate (); *)
   set_active_view i;
   prerr_endline "exiting activate_input"
 
@@ -514,7 +529,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
     buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
     buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
 
-class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs =
+class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
 object(self)
   val input_view = _script
   val input_buffer = _script#buffer
@@ -523,6 +538,7 @@ object(self)
   val message_view = _mv
   val message_buffer = _mv#buffer
   val cmd_stack = _cs
+  val mycoqtop = _ct
   val mutable is_active = false
   val mutable read_only = false
   val mutable filename = None
@@ -742,8 +758,9 @@ object(self)
         try
           Ideproof.display
             (Ideproof.mode_tactic menu_callback)
-            proof_view (Coq.goals Coq.dummy_coqtop)
-        with e -> prerr_endline (Printexc.to_string e)
+            proof_view (Coq.goals mycoqtop)
+        with
+          | e -> prerr_endline (Printexc.to_string e)
       end
 
   method show_goals = self#show_goals_full
@@ -776,12 +793,14 @@ object(self)
       try
         full_goal_done <- false;
         prerr_endline "Send_to_coq starting now";
-        let r = Coq.interp Coq.dummy_coqtop verbosely phrase in
+        let r = Coq.interp mycoqtop verbosely phrase in
         let is_complete = true in
-        let msg = Coq.read_stdout Coq.dummy_coqtop in
+        let msg = Coq.read_stdout mycoqtop in
         sync display_output msg;
         Some (is_complete,r)
-      with e ->
+      with
+        | Coq_failure (l,pp) -> Pervasives.prerr_endline (Coq.msgnl pp); None
+        | e ->
         if show_error then sync display_error e;
         None
 
@@ -974,7 +993,7 @@ object(self)
               cmd_stack;
             Stack.clear cmd_stack;
             self#clear_message)();
-    Coq.reset_initial ()
+    Coq.reset_coqtop mycoqtop
 
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method backtrack_to_no_lock i =
@@ -990,7 +1009,7 @@ object(self)
     in
     begin
       try
-        prerr_endline (string_of_int (rewind Coq.dummy_coqtop (n_step 0)));
+        prerr_endline (string_of_int (Coq.rewind mycoqtop (n_step 0)));
         prerr_endline (string_of_int (Stack.length cmd_stack));
         sync (fun _ ->
                 let start =
@@ -1053,7 +1072,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          ignore ((rewind Coq.dummy_coqtop 1));
+          ignore ((Coq.rewind mycoqtop 1));
           sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
@@ -1117,7 +1136,7 @@ object(self)
   val mutable deact_id = None
   val mutable act_id = None
 
-  method deactivate () =
+  method deactivate () = () (*
     is_active <- false;
     (match act_id with None -> ()
        | Some id ->
@@ -1125,14 +1144,14 @@ object(self)
            input_view#misc#disconnect id;
            prerr_endline "DISCONNECTED old active : ";
            print_id id;
-    )(*;
+    );
     deact_id <- Some
                   (input_view#event#connect#key_press self#disconnected_keypress_handler);
     prerr_endline "CONNECTED  inactive : ";
     print_id (Option.get deact_id)*)
 
   (* XXX *)
-  method activate () =
+  method activate () = if not is_active then begin
     is_active <- true;(*
     (match deact_id with None -> ()
        | Some id -> input_view#misc#disconnect id;
@@ -1148,11 +1167,12 @@ object(self)
     with
       | None -> ()
       | Some f -> let dir = Filename.dirname f in
-          if not (is_in_loadpath Coq.dummy_coqtop dir) then
+          if not (is_in_loadpath mycoqtop dir) then
             begin
-              ignore (Coq.interp Coq.dummy_coqtop false
+              ignore (Coq.interp mycoqtop false
                         (Printf.sprintf "Add LoadPath \"%s\". "  dir))
             end
+  end
 
   method electric_handler =
     input_buffer#connect#insert_text ~callback:
@@ -1340,8 +1360,10 @@ let create_session () =
     GMisc.label ~text:"*scratch*" () in
   let stack =
     Stack.create () in
+  let ct =
+    spawn_coqtop () in
   let legacy_av =
-    new analyzed_view script proof message stack in
+    new analyzed_view script proof message stack ct in
   let _ =
     script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
   let _ =
@@ -1349,6 +1371,9 @@ let create_session () =
   let _ =
     GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
   let _ =
+    List.map (fun (opts,_,_,dflt) -> setopts ct opts dflt) print_items in
+  let _ = legacy_av#activate () in
+  let _ =
     proof#event#connect#motion_notify ~callback:
       (fun e ->
          let win = match proof#get_window `WIDGET with
@@ -1376,7 +1401,8 @@ let create_session () =
       proof_view=proof;
       message_view=message;
       analyzed_view=legacy_av;
-      encoding=""
+      encoding="";
+      toplvl=ct
     }
 
 (* XXX - to be used later
@@ -2193,17 +2219,17 @@ let main files =
 				in
 				let _do_or_activate f () =
 				  let current = session_notebook#current_term in
-				  let analyzed_view = current.analyzed_view in
+				  let analyzed_view = current.analyzed_view in (*
 				    if analyzed_view#is_active then begin
-                                      prerr_endline ("view "^current.tab_label#text^"already active");
-				      ignore (f analyzed_view)
+                                      prerr_endline ("view "^current.tab_label#text^"already active"); *)
+				      ignore (f analyzed_view) (*
                                     end else
 				      begin
 					flash_info "New proof started";
                                         prerr_endline ("activating view "^current.tab_label#text);
 					activate_input session_notebook#current_page;
 					ignore (f analyzed_view)
-				      end
+				      end *)
 				in
 
 				let do_or_activate f =
@@ -2211,7 +2237,8 @@ let main files =
 				    (_do_or_activate
 				       (fun av -> f av;
                                           pop_info ();
-                                          push_info (Coq.current_status Coq.dummy_coqtop)
+                                          let cur_ct = session_notebook#current_term.toplvl in
+                                          push_info (Coq.current_status cur_ct)
                                        )
                                     )
 				in
@@ -2440,8 +2467,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					(* Template for match *)
 					let callback () =
 					  let w = get_current_word () in
+let cur_ct = session_notebook#current_term.toplvl in
 					    try
-					      let cases = Coq.make_cases Coq.dummy_coqtop w
+					      let cases = Coq.make_cases cur_ct w
 					      in
 					      let print c = function
 						| [x] -> Format.fprintf c "  | %s => _@\n" x
@@ -2590,25 +2618,12 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					    ~accel_group
 					    ~accel_modi:!current.modifier_for_display
 					  in
-
-             let print_items = [
-               ([implicit],"Display _implicit arguments",GdkKeysyms._i,false);
-               ([coercions],"Display _coercions",GdkKeysyms._c,false);
-               ([raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
-               ([notations],"Display _notations",GdkKeysyms._n,true);
-               ([all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
-               ([existential],"Display _existential variable instances",GdkKeysyms._e,false);
-               ([universes],"Display _universe levels",GdkKeysyms._u,false);
-               ([all_basic;existential;universes],"Display all _low-level contents",GdkKeysyms._l,false)
-             ] in
-             let setopts opts v = List.iter (fun o -> set Coq.dummy_coqtop o v) opts in
              let _ =
                List.map
                        (fun (opts,text,key,dflt) -> 
-                          setopts opts dflt;
                           view_factory#add_check_item ~key ~active:dflt text
                             ~callback:(fun v -> do_or_activate (fun a ->
-                                                                  setopts opts v;
+                                                                  setopts session_notebook#current_term.toplvl opts v;
                                                                   a#show_goals) ()))
                        print_items
              in
@@ -3068,7 +3083,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
                                                                                  let f = if Filename.check_suffix f ".v" then f else f^".v" in
 										 load_file (fun s -> print_endline s; exit 1) f)
                                                                     files;
-								  activate_input 0
+								 activate_input 0 
 								end
 							      else
 								begin
@@ -3078,6 +3093,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								end;
                                   initial_about session_notebook#current_term.proof_view#buffer;
                                   !show_toolbar !current.show_toolbar;
+                                  Command_windows.get_current_toplevel := (fun () -> session_notebook#current_term.toplvl);
                                   session_notebook#current_term.script#misc#grab_focus ()
 
 ;;
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index bd26bab273..ad122ee2bd 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -54,7 +54,9 @@ object(self)
 
   method pages = term_list
 
-  method current_term = List.nth term_list super#current_page
+  method current_term =
+    List.nth term_list super#current_page
+
 end
 
 let create build =
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 86d29c4be6..b5db04d213 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -25,3 +25,4 @@ Heap
 Option
 Dnet
 Store
+Safe_marshal
diff --git a/lib/safe_marshal.ml b/lib/safe_marshal.ml
index e9ba81b499..0ae5245d7f 100644
--- a/lib/safe_marshal.ml
+++ b/lib/safe_marshal.ml
@@ -5,6 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*
+let uuencode s =
+  let norm_s = s ^ (String.make (String.length s mod 3) '\000') in
+  let rec y f x = f (y f) x in
+  let chop rem = function
+    | "" -> []
+    | s -> String.sub s 0 3 :: (rem (String.sub s 3 (String.length (s - 3)))) in
+  let chunks = y chop norm_s in
+ *)
 
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
 let bohcnv = Array.init 256 (fun i -> i -
@@ -13,7 +22,7 @@ let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x61 <= i then 0x20 else 0))
 
 let hex_of_bin ch = hobcnv.(int_of_char ch)
-let bin_of_hex s = bohcnv.(char_of_int s[0]) * 16 + bohcnv.(char_of_int s[1])
+let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1]))
 
 let send cout expr =
   let mshl_expr = Marshal.to_string expr [] in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74c4ff3db8..440d362807 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 a312b0037b..899cee1e46 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 c74d67f2ce..561821b563 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