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

7 files changed, 103 insertions, 91 deletions

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 ())