[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.

22 files changed, 292 insertions, 232 deletions

diff --git a/API/API.mli b/API/API.mli
index 3ed326ff0..5c421ade4 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5768,8 +5768,11 @@ end
 
 module Stm :
 sig
+  type doc
   type state
-  val state_of_id :
+
+  val get_doc : Feedback.doc_id -> doc
+  val state_of_id : doc:doc ->
     Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 end
 
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))
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 54d16a9be..7a126363c 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,6 +15,7 @@ type level =
   | Warning
   | Error
 
+type doc_id = int
 type route_id = int
 
 type feedback_content =
@@ -35,7 +36,8 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.t
 
 type feedback = {
-  id       : Stateid.t;
+  doc_id   : doc_id;            (* The document being concerned *)
+  span_id  : Stateid.t;
   route    : route_id;
   contents : feedback_content;
 }
@@ -52,23 +54,27 @@ let add_feeder =
 let del_feeder fid = Hashtbl.remove feeders fid
 
 let default_route = 0
-let feedback_id    = ref Stateid.dummy
+let span_id    = ref Stateid.dummy
+let doc_id     = ref 0
 let feedback_route = ref default_route
 
-let set_id_for_feedback ?(route=default_route) i =
-  feedback_id := i; feedback_route := route
+let set_id_for_feedback ?(route=default_route) d i =
+  doc_id := d;
+  span_id := i;
+  feedback_route := route
 
-let feedback ?id ?route what =
+let feedback ?did ?id ?route what =
   let m = {
      contents = what;
-     route = Option.default !feedback_route route;
-     id    = Option.default !feedback_id id;
+     route    = Option.default !feedback_route route;
+     doc_id   = Option.default !doc_id did;
+     span_id  = Option.default !span_id id;
   } in
   Hashtbl.iter (fun _ f -> f m) feeders
 
 (* Logging messages *)
 let feedback_logger ?loc lvl msg =
-  feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg))
+  feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg))
 
 let msg_info    ?loc x = feedback_logger ?loc Info x
 let msg_notice  ?loc x = feedback_logger ?loc Notice x
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 45a02d384..73b84614f 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -17,6 +17,9 @@ type level =
   | Error
 
 
+(** Document unique identifier for serialization *)
+type doc_id = int
+
 (** Coq "semantic" infos obtained during execution *)
 type route_id = int
 
@@ -43,7 +46,8 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.t
 
 type feedback = {
-  id       : Stateid.t;         (* The document part concerned *)
+  doc_id   : doc_id;            (* The document being concerned *)
+  span_id  : Stateid.t;         (* The document part concerned *)
   route    : route_id;          (* Extra routing info *)
   contents : feedback_content;  (* The payload *)
 }
@@ -60,13 +64,13 @@ val add_feeder : (feedback -> unit) -> int
 (** [del_feeder fid] removes the feeder with id [fid] *)
 val del_feeder : int -> unit
 
-(** [feedback ?id ?route fb] produces feedback fb, with [route] and
-    [id] set appropiatedly, if absent, it will use the defaults set by
-    [set_id_for_feedback] *)
-val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
+(** [feedback ?did ?sid ?route fb] produces feedback [fb], with
+    [route] and [did, sid] set appropiatedly, if absent, it will use
+    the defaults set by [set_id_for_feedback] *)
+val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
 
 (** [set_id_for_feedback route id] Set the defaults for feedback *)
-val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
+val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit
 
 (** {6 output functions}
 
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 32494a879..9ae8bfe65 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -367,18 +367,30 @@ let do_profile s call_trace tac =
 
 let get_local_profiling_results () = List.hd Local.(!stack)
 
-module SM = Map.Make(Stateid.Self)
+(* We maintain our own cache of document data, given that the
+   semantics of the STM implies that synchronized state for opaque
+   proofs will be lost on QED. This provides some complications later
+   on as we will have to simulate going back on the document on our
+   own. *)
+module DData = struct
+    type t = Feedback.doc_id * Stateid.t
+    let compare x y = Pervasives.compare x y
+end
+
+module SM = Map.Make(DData)
 
 let data = ref SM.empty
 
 let _ =
   Feedback.(add_feeder (function
-    | { id = s; contents = Custom (_, "ltacprof_results", xml) } ->
+    | { doc_id = d;
+        span_id = s;
+        contents = Custom (_, "ltacprof_results", xml) } ->
         let results = to_ltacprof_results xml in
         let other_results = (* Multi success can cause this *)
-          try SM.find s !data
+          try SM.find (d,s) !data
           with Not_found -> empty_treenode root in
-        data := SM.add s (merge_roots results other_results) !data
+        data := SM.add (d,s) (merge_roots results other_results) !data
     | _ -> ()))
 
 let reset_profile () =
@@ -388,7 +400,10 @@ let reset_profile () =
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
-  let valid id _ = Stm.state_of_id id <> `Expired in
+  (* The STM doesn't provide yet a proper document query and traversal
+     API, thus we need to re-check if some states are current anymore
+     (due to backtracking) using the `state_of_id` API. *)
+  let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index a4b35ad60..b46556ea6 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -11,7 +11,7 @@ open Stm
 module Util : sig
 
 val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
@@ -43,8 +43,8 @@ let simple_goal sigma g gs =
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
-let is_focused_goal_simple id =
-  match state_of_id id with
+let is_focused_goal_simple ~doc id =
+  match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { proof }) ->
        let proof = Proof_global.proof_of_state proof in
@@ -88,8 +88,8 @@ let static_bullet ({ entry_point; prev_node } as view) =
         | _ -> `Stop) entry_point
   | _ -> assert false
 
-let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
-  match is_focused_goal_simple id with
+let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
@@ -116,8 +116,8 @@ let static_curly_brace ({ entry_point; prev_node } as view) =
       `Cont (nesting + 1,node)
     | _ -> `Cont (nesting,node)) (-1, entry_point)
 
-let dynamic_curly_brace { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_curly_brace doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
@@ -138,8 +138,8 @@ let static_par { entry_point; prev_node } =
       Some { block_stop = entry_point.id; block_start = pid;
              dynamic_switch = pid; carry_on_data = unit_val }
 
-let dynamic_par { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_par doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
@@ -167,9 +167,9 @@ let static_indent ({ entry_point; prev_node } as view) =
                    carry_on_data = of_vernac_expr_val entry_point.ast }
         ) last_tac
 
-let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
   Printf.eprintf "%s\n" (Stateid.to_string id);
-  match is_focused_goal_simple id with
+  match is_focused_goal_simple ~doc id with
   | `Simple [] -> `Leaks
   | `Simple focused ->
       let but_last = List.tl (List.rev focused) in 
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index e23a1d1c1..5cff0a8a7 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -21,7 +21,7 @@
     type).  `Simple carries the list of focused goals.
 *)
 val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
 
 type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
 
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 95012d984..a27c6d6cd 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 85f0e6bfc..ac7a270ac 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 2c5e9ed81..220ed9be4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -40,8 +40,8 @@ let state_ready, state_ready_hook = Hook.make
 let forward_feedback, forward_feedback_hook = 
   let m = Mutex.create () in
   Hook.make ~default:(function
-    | { id = id; route; contents } ->
-        try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+    | { doc_id = did; span_id = id; route; contents } ->
+        try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m
         with e -> Mutex.unlock m; raise e) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
@@ -254,6 +254,10 @@ type stm_doc_type =
   | VioDoc      of Names.DirPath.t
   | Interactive of Names.DirPath.t
 
+(* Dummy until we land the functional interp patch + fixed start_library *)
+type doc = int
+let dummy_doc : doc = 0
+
 (* Imperative wrap around VCS to obtain _the_ VCS that is the
  * representation of the document Coq is currently processing *)
 module VCS : sig
@@ -270,7 +274,7 @@ module VCS : sig
 
   type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
-  val init : stm_doc_type -> id -> unit
+  val init : stm_doc_type -> id -> doc
   (* val get_type : unit -> stm_doc_type *)
   val is_interactive : unit -> [`Yes | `No | `Shallow]
   val is_vio_doc : unit -> bool
@@ -460,7 +464,8 @@ end = struct (* {{{ *)
   let init dt id =
     doc_type := dt;
     vcs := empty id;
-    vcs := set_info !vcs id (default_info ())
+    vcs := set_info !vcs id (default_info ());
+    dummy_doc
 
   (* let get_type () = !doc_type *)
 
@@ -682,7 +687,7 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-let state_of_id id =
+let state_of_id ~doc id =
   try match (VCS.get_info id).state with
     | Valid s -> `Valid (Some s)
     | Error (e,_) -> `Error e
@@ -971,7 +976,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
   (* The Stm will gain the capability to interpret commmads affecting
      the whole document state, such as backtrack, etc... so we start
      to design the stm command interpreter now *)
-  set_id_for_feedback ?route id;
+  set_id_for_feedback ?route dummy_doc id;
   Aux_file.record_in_aux_set_at ?loc ();
   (* We need to check if a command should be filtered from
    * vernac_entries, as it cannot handle it. This should go away in
@@ -1137,6 +1142,7 @@ end (* }}} *)
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
+
 let get_hint_ctx loc =
   let s = Aux_file.get ?loc !hints "context_used" in
   match Str.split (Str.regexp ";") s with
@@ -1191,7 +1197,7 @@ type recovery_action = {
 }
 
 type dynamic_block_error_recovery =
-  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+  doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
 
 let proof_block_delimiters = ref []
 
@@ -2132,7 +2138,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       let decl, name = List.hd valid_boxes in
       try
         let _, dynamic_check = List.assoc name !proof_block_delimiters in
-        match dynamic_check decl with
+        match dynamic_check dummy_doc decl with
         | `Leaks -> Exninfo.iraise exn
         | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
            let tac =
@@ -2368,7 +2374,7 @@ type stm_init_options = {
 }
 
 let init { doc_type } =
-  VCS.init doc_type Stateid.initial;
+  let doc = VCS.init doc_type Stateid.initial in
   set_undo_classifier Backtrack.undo_vernac_classifier;
   (* we declare the library here XXX: *)
   State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
@@ -2386,35 +2392,39 @@ let init { doc_type } =
       async_proofs_workers_extra_env := Array.of_list
         (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
     with Not_found -> () end;
-  end
+  end;
+  doc
 
-let observe id =
+let observe ~doc id =
   let vcs = VCS.backup () in
   try
     Reach.known_state ~cache:(VCS.is_interactive ()) id;
-    VCS.print ()
+    VCS.print ();
+    doc
   with e ->
     let e = CErrors.push e in
     VCS.print ();
     VCS.restore vcs;
     Exninfo.iraise e
 
-let finish () =
+let finish ~doc =
   let head = VCS.current_branch () in
-  observe (VCS.get_branch_pos head);
+  let doc =observe ~doc (VCS.get_branch_pos head) in
   VCS.print ();
   (* EJGA: Setting here the proof state looks really wrong, and it
      hides true bugs cf bug #5363. Also, what happens with observe? *)
   (* Some commands may by side effect change the proof mode *)
-  match VCS.get_branch head with
+  (match VCS.get_branch head with
   | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
   | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
   | _ -> ()
+  ); doc
 
-let wait () =
-  finish ();
+let wait ~doc =
+  let doc = finish ~doc in
   Slaves.wait_all_done ();
-  VCS.print ()
+  VCS.print ();
+  doc
 
 let rec join_admitted_proofs id =
   if Stateid.equal id Stateid.initial then () else
@@ -2425,17 +2435,17 @@ let rec join_admitted_proofs id =
        join_admitted_proofs view.next
   | _ -> join_admitted_proofs view.next
 
-let join () =
-  wait ();
+let join ~doc =
+  let doc = wait ~doc in
   stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
   stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
-  VCS.print ()
+  doc
 
 let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
-type document = VCS.vcs
+
 type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
 let check_task name (tasks,rcbackup) i =
   RemoteCounter.restore rcbackup;
@@ -2502,12 +2512,13 @@ let handle_failure (e, info) vcs =
       VCS.print ();
       Exninfo.iraise (e, info)
 
-let snapshot_vio ldir long_f_dot_vo =
-  finish ();
+let snapshot_vio ~doc ldir long_f_dot_vo =
+  let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
-    (Global.opaque_tables ())
+    (Global.opaque_tables ());
+  doc
 
 let reset_task_queue = Slaves.reset_task_queue
 
@@ -2542,7 +2553,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias (oid,x));
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
       | VtBack (false, id), VtNow ->
           stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
@@ -2571,7 +2582,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
                  then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
       | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
@@ -2589,7 +2600,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
           Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
       | VtProofMode _, VtLater ->
           anomaly(str"VtProofMode must be executed VtNow.")
       | VtProofMode mode, VtNow ->
@@ -2607,7 +2618,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record ();
-          finish ();
+          ignore(finish ~doc:dummy_doc);
           `Ok
       | VtProofStep { parallel; proof_block_detection = cblock }, w ->
           let id = VCS.new_node ~id:newtip () in
@@ -2620,14 +2631,14 @@ let process_transaction ?(newtip=Stateid.fresh ())
              If/when and UI will make something useful with this piece of info,
              detection should occur here.
           detect_proof_block id cblock; *)
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
       | VtQed keep, w ->
           let valid = VCS.get_branch_pos head in
           let rc = merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then finish ();
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
           rc
-          
+
       (* Side effect on all branches *)
       | VtUnknown, _ when expr = VernacToplevelControl Drop ->
           stm_vernac_interp (VCS.get_branch_pos head) x; `Ok
@@ -2644,7 +2655,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
 	    | _ -> ReplayCommand x in
 	  VCS.propagate_sideff ~action;
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
       (* Unknown: we execute it, check for open goals and propagate sideeff *)
       | VtUnknown, VtNow ->
@@ -2693,7 +2704,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
     let e = CErrors.push e in
     handle_failure e vcs
 
-let get_ast id =
+let get_ast ~doc id =
   match VCS.visit id with
   | { step = `Cmd { cast = { loc; expr } } }
   | { step = `Fork (({ loc; expr }, _, _, _), _) } 
@@ -2714,7 +2725,7 @@ let stop_worker n = Slaves.cancel_worker n
 *)
 exception End_of_input
 
-let parse_sentence sid pa =
+let parse_sentence ~doc sid pa =
   (* XXX: Should this restore the previous state?
      Using reach here to try to really get to the
      proper state makes the error resilience code fail *)
@@ -2778,7 +2789,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc ->
     eff_indent, len
   ) (0, 0) loc
 
-let add ~ontop ?newtip verb (loc, ast) =
+let add ~doc ~ontop ?newtip verb (loc, ast) =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
     user_err ?loc ~hdr:"Stm.add"
@@ -2791,10 +2802,10 @@ let add ~ontop ?newtip verb (loc, ast) =
   let clas = classify_vernac ast in
   let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
   match process_transaction ?newtip aast clas with
-  | `Ok -> VCS.cur_tip (), `NewTip
-  | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
+  | `Ok -> doc, VCS.cur_tip (), `NewTip
+  | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
 
-let set_perspective id_list = Slaves.set_perspective id_list
+let set_perspective ~doc id_list = Slaves.set_perspective id_list
 
 type focus = {
   start : Stateid.t;
@@ -2802,11 +2813,11 @@ type focus = {
   tip : Stateid.t
 }
 
-let query ~at ~route s =
+let query ~doc ~at ~route s =
   Future.purify (fun s ->
-    if Stateid.equal at Stateid.dummy then finish ()
+    if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
     else Reach.known_state ~cache:`Yes at;
-    let loc, ast = parse_sentence at s in
+    let loc, ast = parse_sentence ~doc at s in
     let indentation, strlen = compute_indentation ?loc at in
     CWarnings.set_current_loc loc;
     let clas = classify_vernac ast in
@@ -2818,7 +2829,7 @@ let query ~at ~route s =
        ignore(process_transaction aast (VtQuery (false, route), VtNow)))
   s
 
-let edit_at id =
+let edit_at ~doc id =
   if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
   let vcs = VCS.backup () in
   let on_cur_branch id =
@@ -2927,7 +2938,7 @@ let edit_at id =
       | false, None, None -> backto id None
     in
     VCS.print ();
-    rc
+    doc, rc
   with e ->
     let (e, info) = CErrors.push e in
     match Stateid.get info with
@@ -2941,15 +2952,14 @@ let edit_at id =
         VCS.print ();
         Exninfo.iraise (e, info)
 
-let backup () = VCS.backup ()
-let restore d = VCS.restore d
+let get_current_state ~doc = VCS.cur_tip ()
 
-let get_current_state () = VCS.cur_tip ()
+let get_doc did = dummy_doc
 
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
-let current_proof_depth () =
+let current_proof_depth ~doc =
   let head = VCS.current_branch () in
   match VCS.get_branch head with
   | { VCS.kind = `Master } -> 0
@@ -2968,7 +2978,7 @@ let proofname b = match VCS.get_branch b with
   | { VCS.kind = (`Proof _| `Edit _) } -> Some b
   | _ -> None
 
-let get_all_proof_names () =
+let get_all_proof_names ~doc =
   List.map unmangle (CList.map_filter proofname (VCS.branches ()))
 
 (* Export hooks *)
diff --git a/stm/stm.mli b/stm/stm.mli
index ea8aecaed..47963e5d8 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -28,11 +28,14 @@ type stm_init_options = {
 *)
 }
 
-val init : stm_init_options -> unit
+(** The type of a STM document *)
+type doc
+
+val init : stm_init_options -> doc
 
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
+val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
   Vernacexpr.vernac_expr Loc.located
 
 (* Reminder: A parsable [pa] is constructed using
@@ -46,14 +49,14 @@ exception End_of_input
    sync, but it will eventually call edit_at on the fly if needed.
    If [newtip] is provided, then the returned state id is guaranteed
    to be [newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
+val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
   bool -> Vernacexpr.vernac_expr Loc.located ->
-  Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+  doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
    throwing away side effects except messages. Feedback will
    be sent with [report_with], which defaults to the dummy state id *)
-val query :
+val query : doc:doc ->
   at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
@@ -66,27 +69,27 @@ val query :
    If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
 *)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
-val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
+val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
 
 (* Evaluates the tip of the current branch *)
-val finish : unit -> unit
+val finish : doc:doc -> doc
 
 (* Internal use (fake_ide) only, do not use *)
-val wait : unit -> unit
+val wait : doc:doc -> doc
 
-val observe : Stateid.t -> unit
+val observe : doc:doc -> Stateid.t -> doc
 
 val stop_worker : string -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
-val join : unit -> unit
+val join : doc:doc -> doc
 
 (* Saves on the disk a .vio corresponding to the current status:
    - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
      of the completed tasks is a failure) *)
-val snapshot_vio : DirPath.t -> string -> unit
+val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)
@@ -101,20 +104,16 @@ val finish_tasks : string ->
     tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
-val get_current_state : unit -> Stateid.t
+val get_current_state : doc:doc -> Stateid.t
 
 (* This returns the node at that position *)
-val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
 
 (* Reorders the task queue putting forward what is in the perspective *)
-val set_perspective : Stateid.t list -> unit
-
-type document
-val backup : unit -> document
-val restore : document -> unit
+val set_perspective : doc:doc -> Stateid.t list -> unit
 
 (** workers **************************************************************** **)
 
@@ -129,20 +128,20 @@ module QueryTask : AsyncTaskQueue.Task
    While checking a proof, if an error occurs in a (valid) block then
    processing can skip the entire block and go on to give feedback
    on the rest of the proof.
-  
+
    static_block_detection and dynamic_block_validation are run when
    the closing block marker is parsed/executed respectively.
-  
+
    static_block_detection is for example called when "}" is parsed and
    declares a block containing all proof steps between it and the matching
    "{".
-  
+
    dynamic_block_validation is called when an error "crosses" the "}" statement.
    Depending on the nature of the goal focused by "{" the block may absorb the
    error or not.  For example if the focused goal occurs in the type of
    another goal, then the block is leaky.
    Note that one can design proof commands that need no dynamic validation.
-  
+
    Example of document:
 
       .. { tac1. tac2. } ..
@@ -150,7 +149,7 @@ module QueryTask : AsyncTaskQueue.Task
    Corresponding DAG:
 
       .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
-                       
+
    Declaration of block  [-------------------------------------------]
 
       start = 5            the first state_id that could fail in the block
@@ -190,7 +189,7 @@ type recovery_action = {
 }
 
 type dynamic_block_error_recovery =
-  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+  doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
 
 val register_proof_block_delimiter :
   Vernacexpr.proof_block_name ->
@@ -219,9 +218,12 @@ type state = {
   proof : Proof_global.state;
   shallow : bool
 }
-val state_of_id :
+
+val get_doc : Feedback.doc_id -> doc
+
+val state_of_id : doc:doc ->
   Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 
 (* Queries for backward compatibility *)
-val current_proof_depth : unit -> int
-val get_all_proof_names : unit -> Id.t list
+val current_proof_depth : doc:doc -> int
+val get_all_proof_names : doc:doc -> Id.t list
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 186c8f8b7..1716ac0c6 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
 
 let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8f676c656..bf22c16cd 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
 let load_rc = ref true
 let no_load_rc () = load_rc := false
 
-let load_rcfile sid =
+let load_rcfile doc sid =
   if !load_rc then
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,8 +43,8 @@ let load_rcfile sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc
-	with Not_found -> sid
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
+	with Not_found -> doc, sid
 	(*
 	Flags.if_verbose
 	  mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
@@ -56,7 +56,7 @@ let load_rcfile sid =
       iraise reraise
   else
     (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
-     sid)
+     doc, sid)
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 1f7fd6ed9..2c275a00d 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -13,7 +13,7 @@ val set_debug : unit -> unit
 val set_rcfile : string -> unit
 
 val no_load_rc : unit -> unit
-val load_rcfile : Stateid.t -> Stateid.t
+val load_rcfile : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 val push_include : string -> Names.DirPath.t -> bool -> unit
 (** [push_include phys_path log_path implicit] *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 444bf8a8f..c16e2751b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -17,7 +17,7 @@ let top_stderr x =
  * entered to be able to report errors without pretty-printing. *)
 
 type input_buffer = {
-  mutable prompt : unit -> string;
+  mutable prompt : Stm.doc -> string;
   mutable str : Bytes.t; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
@@ -52,12 +52,12 @@ let emacs_prompt_endstring   () = if !print_emacs then "</prompt>" else ""
 
 (* Read a char in an input channel, displaying a prompt at every
    beginning of line. *)
-let prompt_char ic ibuf count =
+let prompt_char doc ic ibuf count =
   let bol = match ibuf.bols with
     | ll::_ -> Int.equal ibuf.len ll
     | [] -> Int.equal ibuf.len 0
   in
-  if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
+  if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -70,11 +70,11 @@ let prompt_char ic ibuf count =
 
 (* Reinitialize the char stream (after a Drop) *)
 
-let reset_input_buffer ic ibuf =
+let reset_input_buffer doc ic ibuf =
   ibuf.str <- Bytes.empty;
   ibuf.len <- 0;
   ibuf.bols <- [];
-  ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf));
+  ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -201,10 +201,10 @@ let make_prompt () =
 
    "n |lem1|lem2|lem3| p < "
 *)
-let make_emacs_prompt() =
-  let statnum = Stateid.to_string (Stm.get_current_state ()) in
-  let dpth = Stm.current_proof_depth() in
-  let pending = Stm.get_all_proof_names() in
+let make_emacs_prompt doc =
+  let statnum = Stateid.to_string (Stm.get_current_state ~doc) in
+  let dpth = Stm.current_proof_depth ~doc in
+  let pending = Stm.get_all_proof_names ~doc in
   let pendingprompt =
     List.fold_left
       (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x)
@@ -217,10 +217,10 @@ let make_emacs_prompt() =
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
 let top_buffer =
-  let pr() =
+  let pr doc =
     emacs_prompt_startstring()
     ^ make_prompt()
-    ^ make_emacs_prompt()
+    ^ make_emacs_prompt doc
     ^ emacs_prompt_endstring()
   in
   { prompt = pr;
@@ -232,7 +232,7 @@ let top_buffer =
 
 let set_prompt prompt =
   top_buffer.prompt
-  <- (fun () ->
+  <- (fun doc ->
     emacs_prompt_startstring()
     ^ prompt ()
     ^ emacs_prompt_endstring())
@@ -258,8 +258,8 @@ let rec discard_to_dot () =
     | Stm.End_of_input -> raise Stm.End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence sid input =
-  try Stm.parse_sentence sid input
+let read_sentence ~doc sid input =
+  try Stm.parse_sentence ~doc sid input
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -300,19 +300,19 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
     is caught and handled (i.e. not re-raised).
 *)
 
-let do_vernac sid =
+let do_vernac doc sid =
   top_stderr (fnl());
-  if !print_emacs then top_stderr (str (top_buffer.prompt()));
+  if !print_emacs then top_stderr (str (top_buffer.prompt doc));
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr sid (read_sentence sid (fst input))
+    Vernac.process_expr doc sid (read_sentence ~doc sid (fst input))
   with
     | Stm.End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
-        else (Feedback.msg_error (str "There is no ML toplevel."); sid)
+        else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid)
     (* Exception printing should be done by the feedback listener,
        however this is not yet ready so we rely on the exception for
        now. *)
@@ -321,7 +321,7 @@ let do_vernac sid =
       let loc = Loc.get_loc info in
       let msg = CErrors.iprint (e, info) in
       TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
-      sid
+      doc, sid
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -337,18 +337,18 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
-let rec loop () =
+let rec loop doc =
   Sys.catch_break true;
   try
-    reset_input_buffer stdin top_buffer;
+    reset_input_buffer doc stdin top_buffer;
     (* Be careful to keep this loop tail-recursive *)
-    let rec vernac_loop sid =
-      let nsid = do_vernac sid in
+    let rec vernac_loop doc sid =
+      let ndoc, nsid = do_vernac doc sid in
       loop_flush_all ();
-      vernac_loop nsid
+      vernac_loop ndoc nsid
     (* We recover the current stateid, threading from the caller is
        not possible due exceptions. *)
-    in vernac_loop (Stm.get_current_state ())
+    in vernac_loop doc (Stm.get_current_state ~doc)
   with
     | CErrors.Drop -> ()
     | CErrors.Quit -> exit 0
@@ -358,4 +358,4 @@ let rec loop () =
                   fnl() ++
                   str"Please report" ++
                   strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
-      loop ()
+      loop doc
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 8eaa68914..46dabf995 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -15,7 +15,7 @@ val print_emacs : bool ref
  * entered to be able to report errors without pretty-printing. *)
 
 type input_buffer = {
-  mutable prompt : unit -> string;
+  mutable prompt : Stm.doc -> string;
   mutable str : Bytes.t; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of begining of lines *)
@@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
 
-val do_vernac : Stateid.t -> Stateid.t
+val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 
-val loop : unit -> unit
+val loop : Stm.doc -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0624c9bed..9b58c9a65 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -81,14 +81,14 @@ let toploop_init = ref begin fun x ->
 let coqtop_init_feed = Coqloop.coqloop_feed
 
 (* Default toplevel loop *)
-let console_toploop_run () =
+let console_toploop_run doc =
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  Coqloop.loop();
+  Coqloop.loop doc;
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
@@ -121,11 +121,6 @@ let print_memory_stat () =
 let _ = at_exit print_memory_stat
 
 (******************************************************************************)
-(* Deprecated                                                                 *)
-(******************************************************************************)
-let _remove_top_ml () = Mltop.remove ()
-
-(******************************************************************************)
 (* Engagement                                                                 *)
 (******************************************************************************)
 let impredicative_set = ref Declarations.PredicativeSet
@@ -183,15 +178,15 @@ let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
   load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
 
-let load_vernacular sid =
+let load_vernacular doc sid =
   List.fold_left
-    (fun sid (f_in, verbosely) ->
+    (fun (doc,sid) (f_in, verbosely) ->
       let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-	Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid) f_in
+	Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
       else
-	Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid s)
-    sid (List.rev !load_vernacular_list)
+	Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+    (doc, sid) (List.rev !load_vernacular_list)
 
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
@@ -258,20 +253,20 @@ let add_compile verbose s =
   in
   compile_list := (verbose,s) :: !compile_list
 
-let compile_file mode (verbosely,f_in) =
+let compile_file mode doc (verbosely,f_in) =
   if !Flags.beautify then
-    Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~f_in ~f_out:None) f_in
+    Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None) f_in
   else
-    Vernac.compile ~verbosely ~mode ~f_in ~f_out:None
+    Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None
 
-let compile_files () =
+let compile_files doc =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
     let mode = !compilation_mode in
     List.iter (fun vf ->
         States.unfreeze init_state;
-        compile_file mode vf)
+        compile_file mode doc vf)
       (List.rev !compile_list)
 
 (******************************************************************************)
@@ -283,7 +278,8 @@ let add_vio_task f =
   set_batch_mode ();
   Flags.quiet := true;
   vio_tasks := f :: !vio_tasks
-let check_vio_tasks () =
+
+let check_vio_tasks doc =
   let rc =
     List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
       true (List.rev !vio_tasks) in
@@ -307,7 +303,7 @@ let set_vio_checking_j opt j =
     prerr_endline "setting the J variable like in 'make vio2vo J=3'";
     exit 1
 
-let schedule_vio_checking () =
+let schedule_vio_checking doc =
   if !vio_files <> [] && !vio_checking then
     Vio_checking.schedule_vio_checking !vio_files_j !vio_files
 
@@ -649,7 +645,7 @@ let init_toplevel arglist =
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
   Lib.init();
-  begin
+  let doc = begin
     try
       let extras = parse_args arglist in
       (* If we have been spawned by the Spawn module, this has to be done
@@ -677,27 +673,29 @@ let init_toplevel arglist =
       then Declaremods.start_library !toplevel_name;
       load_vernac_obj ();
       require ();
-      Stm.(init { doc_type = Interactive Names.DirPath.empty });
-      let sid  = Coqinit.load_rcfile (Stm.get_current_state ()) in
+      let doc = Stm.(init { doc_type = Interactive Names.DirPath.empty }) in
+      let doc, sid = Coqinit.load_rcfile doc (Stm.get_current_state ~doc) in
       (* XXX: We ignore this for now, but should be threaded to the toplevels *)
-      let _sid = load_vernacular sid in
-      compile_files ();
+      let doc, _sid = load_vernacular doc sid in
+      compile_files doc;
       (* All these tasks use coqtop as a driver to invoke more coqtop,
        * they should be really orthogonal to coqtop.
        *)
-      schedule_vio_checking ();
+      schedule_vio_checking doc;
       schedule_vio_compilation ();
-      check_vio_tasks ();
-      outputstate ()
+      check_vio_tasks doc;
+      outputstate ();
+      doc
     with any ->
       flush_all();
-      let extra =
-        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
-        then None
-        else Some (str "Error during initialization: ")
+      let extra = None
+        (* XXX: Must refine once Stm.init takes care of the start_library & friends *)
+        (* if !batch_mode && not Stateid.(equal (Stm.get_current_state ~doc) dummy) *)
+        (* then None *)
+        (* else Some (str "Error during initialization: ") *)
       in
       fatal_error ?extra any
-  end;
+  end in
   if !batch_mode then begin
     flush_all();
     if !output_context then
@@ -705,13 +703,14 @@ let init_toplevel arglist =
     Profile.print_profile ();
     exit 0
   end;
-  Feedback.del_feeder init_feeder
+  Feedback.del_feeder init_feeder;
+  doc
 
 let start () =
-  let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
+  let doc = init_toplevel (List.tl (Array.to_list Sys.argv)) in
   (* In batch mode, Coqtop has already exited at this point. In interactive one,
      dump glob is nothing but garbage ...  *)
-  !toploop_run ();
+  !toploop_run doc;
   exit 1
 
 (* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ac2be7e16..4c26a6ebc 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,11 +11,11 @@
    state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
-val init_toplevel : string list -> unit
+val init_toplevel : string list -> Stm.doc
 
 val start : unit -> unit
 
 (* For other toploops *)
 val toploop_init : (string list -> string list) ref
-val toploop_run : (unit -> unit) ref
+val toploop_run : (Stm.doc -> unit) ref
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cb89dc8ff..1e09a1c0d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -113,13 +113,13 @@ let vernac_error msg =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac ~check ~interactive sid (loc,com) =
+let rec interp_vernac ~check ~interactive doc sid (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-        load_vernac ~verbosely ~check ~interactive sid f
+        load_vernac ~verbosely ~check ~interactive doc sid f
     | v ->
 
       (* XXX: We need to run this before add as the classification is
@@ -137,7 +137,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) =
       in
       CWarnings.set_flags wflags;
 
-      let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
+      let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
       if ntip <> `NewTip then
@@ -146,7 +146,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) =
       (* Due to bug #5363 we cannot use observe here as we should,
          it otherwise reveals bugs *)
       (* Stm.observe nsid; *)
-      if check then Stm.finish ();
+      let ndoc = if check then Stm.finish ~doc else doc in
 
       (* We could use a more refined criteria that depends on the
          vernac. For now we imitate the old approach and rely on the
@@ -155,7 +155,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) =
                         is_proof_step && Proof_global.there_are_pending_proofs () in
 
       if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
-      nsid
+      ndoc, nsid
   in
     try
       (* The -time option is only supported from console-based
@@ -166,7 +166,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) =
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
-      if interactive then ignore(Stm.edit_at sid);
+      if interactive then ignore(Stm.edit_at ~doc sid);
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
@@ -175,7 +175,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~verbosely ~check ~interactive sid file =
+and load_vernac ~verbosely ~check ~interactive doc sid file =
   let ft_beautify, close_beautify =
     if !Flags.beautify_file then
       let chan_beautify = open_out (file^beautify_suffix) in
@@ -187,12 +187,13 @@ and load_vernac ~verbosely ~check ~interactive sid file =
   let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
   let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rsid = ref sid in
+  let rdoc = ref doc in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc, ast =
-          Stm.parse_sentence !rsid in_pa
+          Stm.parse_sentence ~doc:!rdoc !rsid in_pa
         (* If an error in parsing occurs, we propagate the exception
            so the caller of load_vernac will take care of it. However,
            in the future it could be possible that we want to handle
@@ -216,10 +217,11 @@ and load_vernac ~verbosely ~check ~interactive sid file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let nsid = Flags.silently (interp_vernac ~check ~interactive !rsid) (loc, ast) in
-      rsid := nsid
+      let ndoc, nsid = Flags.silently (interp_vernac ~check ~interactive !rdoc !rsid) (loc, ast) in
+      rsid := nsid;
+      rdoc := ndoc
     done;
-    !rsid
+    !rdoc, !rsid
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     close_in in_chan;
@@ -230,7 +232,7 @@ and load_vernac ~verbosely ~check ~interactive sid file =
           if !Flags.beautify then
             pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None;
           if !Flags.beautify_file then close_beautify ();
-          !rsid
+          !rdoc, !rsid
       | reraise ->
          if !Flags.beautify_file then close_beautify ();
 	 iraise (disable_drop e, info)
@@ -242,9 +244,9 @@ and load_vernac ~verbosely ~check ~interactive sid file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr sid loc_ast =
+let process_expr doc sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac ~interactive:true ~check:true sid loc_ast
+  interp_vernac ~interactive:true ~check:true doc sid loc_ast
 
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
@@ -284,7 +286,7 @@ let ensure_exists f =
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 
 (* Compile a vernac file *)
-let compile ~verbosely ~mode ~f_in ~f_out=
+let compile ~verbosely ~mode ~doc ~f_in ~f_out=
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (List.is_empty pfs) then
@@ -310,8 +312,8 @@ let compile ~verbosely ~mode ~f_in ~f_out=
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let _ = load_vernac ~verbosely ~check:true ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
-      Stm.join ();
+      let _ = load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let _doc = Stm.join ~doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
       Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
@@ -329,10 +331,10 @@ let compile ~verbosely ~mode ~f_in ~f_out=
       let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_vio;
-      let _ = load_vernac ~verbosely ~check:false ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
-      Stm.finish ();
+      let _ = load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc = Stm.finish ~doc in
       check_pending_proofs ();
-      Stm.snapshot_vio ldir long_f_dot_vio;
+      let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
       Stm.reset_task_queue ()
   | Vio2Vo ->
       let open Filename in
@@ -343,7 +345,7 @@ let compile ~verbosely ~mode ~f_in ~f_out=
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile ~verbosely ~mode ~f_in ~f_out =
+let compile ~verbosely ~mode ~doc ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile ~verbosely ~mode ~f_in ~f_out;
+  compile ~verbosely ~mode ~doc ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 410dcf0d4..d3a45ce9d 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,14 +12,14 @@
     expected to handle and print errors in form of exceptions, however
     care is taken so the state machine is left in a consistent
     state. *)
-val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
+val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t
+val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
 
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
-val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit
+val compile : verbosely:bool -> mode:compilation_mode -> doc:Stm.doc -> f_in:string -> f_out:string option -> unit