1 files changed, 46 insertions, 28 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 8218302038..65b446ca00 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -113,9 +113,9 @@ let coqide_cmd_checks (loc,ast) =
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
 let interp (id,raw,verbosely,s) =
-  Pp.set_id_for_feedback id;
+  set_id_for_feedback (Interface.Edit id);
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let loc_ast = Vernac.parse_sentence (pa,None) in
+  let loc, ast as loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
   Flags.make_silent (not verbosely);
   if id = 0 then Vernac.eval_expr (loc, VernacStm (Command ast))
@@ -191,6 +191,9 @@ let process_goal sigma g =
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let goals () =
+  Stm.finish ();
+  let s = read_stdout () in
+  if s <> "" then msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     let (goals, zipper, sigma) = Proof.proof pfts in
@@ -206,6 +209,9 @@ let goals () =
 
 let evars () =
   try
+    Stm.finish ();
+    let s = read_stdout () in
+    if s <> "" then msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evarutil.non_instantiated sigma in
@@ -228,15 +234,20 @@ let hints () =
       Some (hint_hyps, hint_goal)
   with Proof_global.NoCurrentProof -> None
 
+
 (** Other API calls *)
 
 let inloadpath dir =
   Loadpath.is_in_load_paths (CUnix.physical_path_of_string dir)
 
-let status () =
+let status force =
   (** We remove the initial part of the current [DirPath.t]
       (usually Top in an interactive session, cf "coqtop -top"),
       and display the other parts (opened sections and modules) *)
+  Stm.finish ();
+  if force then Stm.join ();
+  let s = read_stdout () in
+  if s <> "" then msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -253,7 +264,6 @@ let status () =
     Interface.status_path = path;
     Interface.status_proofname = proof;
     Interface.status_allproofs = allproofs;
-    Interface.status_statenum = Lib.current_command_label ();
     Interface.status_proofnum = Stm.current_proof_depth ();
   }
 
@@ -272,6 +282,8 @@ let set_options options =
   in
   List.iter iter options
 
+let mkcases s = Vernacentries.make_cases s
+
 let about () = {
   Interface.coqtop_version = Coq_config.version;
   Interface.protocol_version = Serialize.protocol_version;
@@ -288,7 +300,16 @@ let handle_exn e =
   match e with
   | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
   | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
-  | e -> dummy, loc_of e, mk_msg e
+  | e ->
+      match Stateid.get_state_id e with
+      | Some (valid, _) -> valid, loc_of e, mk_msg e
+      | None -> dummy, loc_of e, mk_msg e
+
+let init =
+  let initialized = ref false in
+  fun () ->
+   if !initialized then anomaly (str "Already initialized")
+   else (initialized := true; Stm.get_current_state ())
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
@@ -298,29 +319,19 @@ let quit = ref false
 
 (** Grouping all call handlers together + error handling *)
 
-let eval_call c =
-  let handle_exn e =
-    catch_break := false;
-    match e with
-      | Errors.Drop -> None, "Drop is not allowed by coqide!"
-      | Errors.Quit -> None, "Quit is not allowed by coqide!"
-      | e ->
-        let loc = match Loc.get_loc e with
-          | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
-          | _ -> None
-        in
-        loc, (read_stdout ())^"\n"^(string_of_ppcmds (Errors.print e))
-  in
+let eval_call xml_oc log c =
   let interruptible f x =
     catch_break := true;
     Util.check_for_interrupt ();
     let r = f x in
     catch_break := false;
+    let out = read_stdout () in
+    if out <> "" then log (str out);
     r
   in
   let handler = {
     Interface.interp = interruptible interp;
-    Interface.rewind = interruptible (fun _ -> 0);
+    Interface.backto = interruptible backto;
     Interface.goals = interruptible goals;
     Interface.evars = interruptible evars;
     Interface.hints = interruptible hints;
@@ -331,28 +342,35 @@ let eval_call c =
     Interface.set_options = interruptible set_options;
     Interface.mkcases = interruptible Vernacentries.make_cases;
     Interface.quit = (fun () -> quit := true);
+    Interface.init = interruptible init;
     Interface.about = interruptible about;
     Interface.handle_exn = handle_exn; }
   in
-  (* If the messages of last command are still there, we remove them *)
-  ignore (read_stdout ());
   Serialize.abstract_eval_call handler c
 
 (** Message dispatching. *)
+let print_xml =
+  let m = Mutex.create () in
+  fun oc xml ->
+    Mutex.lock m;
+    try Xml_printer.print oc xml; Mutex.unlock m
+    with e -> let e = Errors.push e in Mutex.unlock m; raise e
+  
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = Pp.string_of_ppcmds (hov 0 message) in
+  let msg = string_of_ppcmds (hov 0 message) in
   let message = {
     Interface.message_level = level;
     Interface.message_content = msg;
   } in
+  let () = pr_debug (Printf.sprintf "-> %S" msg) in
   let xml = Serialize.of_message message in
-  Xml_printer.print xml_oc xml
+  print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
   let xml = Serialize.of_feedback msg in
-  Xml_printer.print xml_oc xml
+  print_xml xml_oc xml
 
 (** The main loop *)
 
@@ -366,8 +384,8 @@ let loop () =
   let xml_oc = Xml_printer.make (Xml_printer.TChannel !orig_stdout) in
   let xml_ic = Xml_parser.make (Xml_parser.SChannel stdin) in
   let () = Xml_parser.check_eof xml_ic false in
-  Pp.set_logger (slave_logger xml_oc);
-  Pp.set_feeder (slave_feeder xml_oc);
+  set_logger (slave_logger xml_oc);
+  set_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -377,9 +395,9 @@ let loop () =
       let xml_query = Xml_parser.parse xml_ic in
       let q = Serialize.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call q in
+      let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in
       let () = pr_debug_answer q r in
-      Xml_printer.print xml_oc (Serialize.of_answer q r);
+      print_xml xml_oc (Serialize.of_answer q r);
       flush !orig_stdout
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->