Merge PR #1087: [stm] Switch to a functional API

8 files changed, 98 insertions, 97 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8f676c656b..bf22c16cd3 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 1f7fd6ed95..2c275a00d3 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 444bf8a8f7..c16e2751bc 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 8eaa68914e..46dabf995d 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 0624c9bed8..9b58c9a654 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 ac2be7e161..4c26a6ebcc 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 cb89dc8ff9..1e09a1c0d2 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 410dcf0d46..d3a45ce9de 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