[stm] Switch to a functional API

We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.

For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.

Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.

3 files changed, 43 insertions, 24 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 0dd08293c..ded28a998 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -422,7 +422,7 @@ object(self)
     let rec eat_feedback n =
       if n = 0 then true else
       let msg = Queue.pop feedbacks in
-      let id = msg.id in
+      let id = msg.span_id in
       let sentence =
         let finder _ state_id s =
           match state_id, id with
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index f00b1e142..7cbab56d4 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -76,10 +76,16 @@ let ide_cmd_checks ~id (loc,ast) =
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
+let ide_doc = ref None
+let get_doc () = Option.get !ide_doc
+let set_doc doc = ide_doc := Some doc
+
 let add ((s,eid),(sid,verbose)) =
+  let doc = get_doc () in
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let loc_ast = Stm.parse_sentence sid pa in
-  let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
+  let loc_ast = Stm.parse_sentence ~doc sid pa in
+  let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
+  set_doc doc;
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
   ide_cmd_checks ~id:newid loc_ast;
   (* TODO: the "" parameter is a leftover of the times the protocol
@@ -94,9 +100,10 @@ let add ((s,eid),(sid,verbose)) =
   newid, (rc, "")
 
 let edit_at id =
-  match Stm.edit_at id with
-  | `NewTip -> CSig.Inl ()
-  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))
+  let doc = get_doc () in
+  match Stm.edit_at ~doc id with
+  | doc, `NewTip -> set_doc doc; CSig.Inl ()
+  | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip))
 
 (* TODO: the "" parameter is a leftover of the times the protocol
  * used to include stderr/stdout output.
@@ -109,12 +116,14 @@ let edit_at id =
  *)
 let query (route, (s,id)) =
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  Stm.query ~at:id ~route pa
+  let doc = get_doc () in
+  Stm.query ~at:id ~doc ~route pa
 
 let annotate phrase =
+  let doc = get_doc () in
   let (loc, ast) =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
-    Stm.parse_sentence (Stm.get_current_state ()) pa
+    Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
   in
   (* XXX: Width should be a parameter of annotate... *)
   Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
@@ -196,7 +205,8 @@ let export_pre_goals pgs =
   }
 
 let goals () =
-  Stm.finish ();
+  let doc = get_doc () in
+  set_doc @@ Stm.finish ~doc;
   try
     let pfts = Proof_global.give_me_the_proof () in
     Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
@@ -204,7 +214,8 @@ let goals () =
 
 let evars () =
   try
-    Stm.finish ();
+    let doc = get_doc () in
+    set_doc @@ Stm.finish ~doc;
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
@@ -230,12 +241,17 @@ let hints () =
 
 (** Other API calls *)
 
+let wait () =
+  let doc = get_doc () in
+  set_doc (Stm.wait ~doc)
+
 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 ();
+  set_doc (Stm.finish ~doc:(get_doc ()));
+  if force then
+    set_doc (Stm.join ~doc:(get_doc ()));
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -252,7 +268,7 @@ let status force =
     Interface.status_path = path;
     Interface.status_proofname = proof;
     Interface.status_allproofs = allproofs;
-    Interface.status_proofnum = Stm.current_proof_depth ();
+    Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ());
   }
 
 let export_coq_object t = {
@@ -356,22 +372,23 @@ let init =
   fun file ->
    if !initialized then anomaly (str "Already initialized.")
    else begin
-     let init_sid = Stm.get_current_state () in
+     let init_sid = Stm.get_current_state ~doc:(get_doc ()) in
      initialized := true;
      match file with
      | None -> init_sid
      | Some file ->
          let dir = Filename.dirname file in
          let open Loadpath in let open CUnix in
-         let initial_id, _ =
+         let doc, initial_id, _ =
+           let doc = get_doc () in
            if not (is_in_load_paths (physical_path_of_string dir)) then begin
              let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in
-             let loc_ast = Stm.parse_sentence init_sid pa in
-             Stm.add false ~ontop:init_sid loc_ast
-           end else init_sid, `NewTip in
+             let loc_ast = Stm.parse_sentence ~doc init_sid pa in
+             Stm.add false ~doc ~ontop:init_sid loc_ast
+           end else doc, init_sid, `NewTip in
          if Filename.check_suffix file ".v" then
            Stm.set_compilation_hints file;
-         Stm.finish ();
+         set_doc (Stm.finish ~doc);
          initial_id
    end
 
@@ -413,7 +430,7 @@ let eval_call c =
     Interface.quit = (fun () -> quit := true);
     Interface.init = interruptible init;
     Interface.about = interruptible about;
-    Interface.wait = interruptible Stm.wait;
+    Interface.wait = interruptible wait;
     Interface.interp = interruptible interp;
     Interface.handle_exn = handle_exn;
     Interface.stop_worker = Stm.stop_worker;
@@ -449,7 +466,8 @@ let msg_format = ref (fun () ->
     Xmlprotocol.Richpp margin
 )
 
-let loop () =
+let loop doc =
+  set_doc doc;
   init_signal_handler ();
   catch_break := false;
   let in_ch, out_ch = Spawned.get_channels ()                        in
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index b452b0a13..aaa24a2a9 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -939,7 +939,7 @@ let of_edit_or_state_id id = ["object","state"], of_stateid id
 
 let of_feedback msg =
   let content = of_feedback_content msg.contents in
-  let obj, id = of_edit_or_state_id msg.id in
+  let obj, id = of_edit_or_state_id msg.span_id in
   let route = string_of_int msg.route in
   Element ("feedback", obj @ ["route",route], [id;content])
 
@@ -947,8 +947,9 @@ let of_feedback msg_fmt =
   msg_format := msg_fmt; of_feedback
 
 let to_feedback xml = match xml with
-  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
-      id = to_stateid id;
+  | Element ("feedback", ["object","state";"route",route], [id;content]) -> {
+      doc_id = 0;
+      span_id = to_stateid id;
       route = int_of_string route;
       contents = to_feedback_content content }
   | x -> raise (Marshal_error("feedback",x))