Merge PR#441: Port Toplevel to the Stm API

7 files changed, 128 insertions, 193 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index ffd0d7805..2b9a04dad 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() =
+let load_rcfile sid =
   if !load_rc then
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac false !rcfile
+          Vernac.load_vernac false sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,8 +43,8 @@ let load_rcfile() =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac false inferedrc
-	with Not_found -> ()
+          Vernac.load_vernac false sid inferedrc
+	with Not_found -> sid
 	(*
 	Flags.if_verbose
 	  mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
@@ -55,7 +55,8 @@ let load_rcfile() =
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
   else
-    Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.")
+    (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
+     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 4ff87628c..3b42289ee 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 : unit -> unit
+val load_rcfile : Stateid.t -> 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 2282932d4..4641a2bc8 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -7,11 +7,6 @@
 (************************************************************************)
 
 open Pp
-open CErrors
-open Util
-open Flags
-open Vernac
-open Pcoq
 
 let top_stderr x =
   Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
@@ -24,7 +19,7 @@ type input_buffer = {
   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 *)
-  mutable tokens : Gram.coq_parsable; (* stream of tokens *)
+  mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -61,7 +56,7 @@ let prompt_char ic ibuf count =
     | 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 !Flags.print_emacs then top_stderr (str (ibuf.prompt()));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -78,7 +73,7 @@ let reset_input_buffer ic ibuf =
   ibuf.str <- Bytes.empty;
   ibuf.len <- 0;
   ibuf.bols <- [];
-  ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
+  ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -89,7 +84,7 @@ module TopErr = struct
 
 let get_bols_of_loc ibuf (bp,ep) =
   let add_line (b,e) lines =
-    if b < 0 || e < b then anomaly (Pp.str "Bad location");
+    if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location");
     match lines with
       | ([],None) -> ([], Some (b,e))
       | (fl,oe) -> ((b,e)::fl, oe)
@@ -174,7 +169,7 @@ let error_info_for_buffer ?loc buf =
       let fname = loc.Loc.fname in
       let hl, loc =
         (* We are in the toplevel *)
-        if String.equal fname "" then
+        if CString.equal fname "" then
           let nloc = adjust_loc_buf buf loc in
           if valid_buffer_loc buf loc then
             (fnl () ++ print_highlight_location buf nloc, nloc)
@@ -223,7 +218,7 @@ let make_emacs_prompt() =
   let pending = Stm.get_all_proof_names() in
   let pendingprompt =
     List.fold_left
-      (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x)
+      (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x)
       "" pending in
   let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
   if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
@@ -243,7 +238,7 @@ let top_buffer =
     str = Bytes.empty;
     len = 0;
     bols = [];
-    tokens = Gram.parsable (Stream.of_list []);
+    tokens = Pcoq.Gram.parsable (Stream.of_list []);
     start = 0 }
 
 let set_prompt prompt =
@@ -257,10 +252,10 @@ let set_prompt prompt =
 let parse_to_dot =
   let rec dot st = match Stream.next st with
     | Tok.KEYWORD ("."|"...") -> ()
-    | Tok.EOI -> raise End_of_input
+    | Tok.EOI -> raise Stm.End_of_input
     | _ -> dot st
   in
-  Gram.Entry.of_parser "Coqtoplevel.dot" dot
+  Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot
 
 (* If an error occurred while parsing, we try to read the input until a dot
    token is encountered.
@@ -268,21 +263,19 @@ let parse_to_dot =
 
 let rec discard_to_dot () =
   try
-    Gram.entry_parse parse_to_dot top_buffer.tokens
+    Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens
   with
     | Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
-    | End_of_input -> raise End_of_input
+    | Stm.End_of_input -> raise Stm.End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence input =
-  try
-    let (loc, _ as r) = Vernac.parse_sentence input in
-    CWarnings.set_current_loc loc; r
+let read_sentence sid input =
+  try Stm.parse_sentence sid input
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
     TopErr.print_toplevel_parse_error reraise top_buffer;
-    iraise reraise
+    Exninfo.iraise reraise
 
 (** Coqloop Console feedback handler *)
 let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
@@ -312,25 +305,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
     is caught and handled (i.e. not re-raised).
 *)
 
-let do_vernac () =
+let do_vernac sid =
   top_stderr (fnl());
-  if !print_emacs then top_stderr (str (top_buffer.prompt()));
+  if !Flags.print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr top_buffer.tokens (read_sentence input)
+    Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input))
   with
-    | End_of_input | CErrors.Quit ->
+    | 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.")
+        else (Feedback.msg_error (str "There is no ML toplevel."); sid)
     (* Exception printing is done now by the feedback listener. *)
     (* XXX: We need this hack due to the side effects of the exception
        printer and the reliance of Stm.define on attaching crutial
        state to exceptions *)
-    | any -> ignore (CErrors.(iprint (push any)))
-
+    | any -> ignore (CErrors.(iprint (push any))); sid
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -348,11 +340,16 @@ let loop_flush_all () =
 
 let rec loop () =
   Sys.catch_break true;
-  if !Flags.print_emacs then Vernacentries.qed_display_script := false;
-  Flags.coqtop_ui := true;
   try
     reset_input_buffer stdin top_buffer;
-    while true do do_vernac(); loop_flush_all () done
+    (* Be careful to keep this loop tail-recursive *)
+    let rec vernac_loop sid =
+      let nsid = do_vernac sid in
+      loop_flush_all ();
+      vernac_loop nsid
+    (* We recover the current stateid, threading from the caller is
+       not possible due exceptions. *)
+    in vernac_loop (Stm.get_current_state ())
   with
     | CErrors.Drop -> ()
     | CErrors.Quit -> exit 0
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 8a34ded6d..66bbf43f6 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
 
-val do_vernac : unit -> unit
+val do_vernac : Stateid.t -> Stateid.t
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index aca94e63d..c259beb17 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -8,11 +8,8 @@
 
 open Pp
 open CErrors
-open Util
 open Flags
-open Names
 open Libnames
-open States
 open Coqinit
 
 let () = at_exit flush_all
@@ -133,10 +130,10 @@ let engage () =
 
 let set_batch_mode () = batch_mode := true
 
-let toplevel_default_name = DirPath.make [Id.of_string "Top"]
+let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
 let toplevel_name = ref toplevel_default_name
 let set_toplevel_name dir =
-  if DirPath.is_empty dir then error "Need a non empty toplevel module name";
+  if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name";
   toplevel_name := dir
 
 let remove_top_ml () = Mltop.remove ()
@@ -150,9 +147,9 @@ let set_inputstate s =
   warn_deprecated_inputstate ();
   inputstate:=s
 let inputstate () =
-  if not (String.is_empty !inputstate) then
+  if not (CString.is_empty !inputstate) then
     let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
-    intern_state fname
+    States.intern_state fname
 
 let warn_deprecated_outputstate =
   CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
@@ -164,9 +161,9 @@ let set_outputstate s =
   warn_deprecated_outputstate ();
   outputstate:=s
 let outputstate () =
-  if not (String.is_empty !outputstate) then
+  if not (CString.is_empty !outputstate) then
     let fname = CUnix.make_suffix !outputstate ".coq" in
-    extern_state fname
+    States.extern_state fname
 
 let set_include d p implicit =
   let p = dirpath_of_string p in
@@ -175,15 +172,15 @@ let set_include d p implicit =
 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 () =
-  List.iter
-    (fun (s,b) ->
+let load_vernacular sid =
+  List.fold_left
+    (fun sid (s,v) ->
       let s = Loadpath.locate_file s in
       if !Flags.beautify then
-	with_option beautify_file (Vernac.load_vernac b) s
+	with_option beautify_file (Vernac.load_vernac v sid) s
       else
-	Vernac.load_vernac b s)
-    (List.rev !load_vernacular_list)
+	Vernac.load_vernac v sid s)
+    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
@@ -250,7 +247,6 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
-  Vernacentries.qed_display_script := false;
   color := `OFF
 
 (** Options for CoqIDE *)
@@ -380,7 +376,7 @@ let get_host_port opt s =
 let get_error_resilience opt = function
   | "on" | "all" | "yes" -> `All
   | "off" | "no" -> `None
-  | s -> `Only (String.split ',' s)
+  | s -> `Only (CString.split ',' s)
 
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
@@ -625,7 +621,7 @@ let init_toplevel arglist =
       init_load_path ();
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
-      if not (List.is_empty extras) then begin
+      if not (CList.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
         prerr_endline "See -help for the list of supported options";
         exit 1
@@ -634,15 +630,16 @@ let init_toplevel arglist =
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      if (not !batch_mode || List.is_empty !compile_list)
+      if (not !batch_mode || CList.is_empty !compile_list)
          && Global.env_is_initial ()
       then Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();
       Stm.init ();
-      load_rcfile();
-      load_vernacular ();
+      let sid  = load_rcfile (Stm.get_current_state ()) in
+      (* XXX: We ignore this for now, but should be threaded to the toplevels *)
+      let _sid = load_vernacular sid in
       compile_files ();
       schedule_vio_checking ();
       schedule_vio_compilation ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9917a49b4..98458a57a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -13,111 +13,30 @@ open CErrors
 open Util
 open Flags
 open Vernacexpr
+open Vernacprop
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-let user_error loc s = CErrors.user_err ~loc (str s)
-
-(* Navigation commands are allowed in a coqtop session but not in a .v file *)
-
-let rec is_navigation_vernac = function
-  | VernacResetInitial
-  | VernacResetName _
-  | VernacBacktrack _
-  | VernacBackTo _
-  | VernacBack _
-  | VernacStm _ -> true
-  | VernacRedirect (_, (_,c))
-  | VernacTime (_,c) ->
-      is_navigation_vernac c (* Time Back* is harmless *)
-  | c -> is_deep_navigation_vernac c
-
-and is_deep_navigation_vernac = function
-  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | _ -> false
-
-(* NB: Reset is now allowed again as asked by A. Chlipala *)
-
-let is_reset = function
-  | VernacResetInitial | VernacResetName _ -> true
-  | _ -> false
-
-let checknav_simple loc cmd =
+let checknav_simple (loc, cmd) =
   if is_navigation_vernac cmd && not (is_reset cmd) then
-    user_error loc "Navigation commands forbidden in files."
+    CErrors.user_err ~loc (str "Navigation commands forbidden in files.")
 
-let checknav_deep loc ast =
+let checknav_deep (loc, ast) =
   if is_deep_navigation_vernac ast then
-    user_error loc "Navigation commands forbidden in nested commands."
-
-(* When doing Load on a file, two behaviors are possible:
-
-   - either the history stack is grown by only one command,
-     the "Load" itself. This is mandatory for command-counting
-     interfaces (CoqIDE).
-
-   - either each individual sub-commands in the file is added
-     to the history stack. This allows commands like Show Script
-     to work across the loaded file boundary (cf. bug #2820).
-
-   The best of the two could probably be combined someday,
-   in the meanwhile we use a flag. *)
-
-let atomic_load = ref true
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "atomic registration of commands in a Load";
-      Goptions.optkey   = ["Atomic";"Load"];
-      Goptions.optread  = (fun () -> !atomic_load);
-      Goptions.optwrite = ((:=) atomic_load) }
+    CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.")
 
 let disable_drop = function
   | Drop -> CErrors.error "Drop is forbidden."
   | e -> e
 
-(* Opening and closing a channel. Open it twice when verbose: the first
-   channel is used to read the commands, and the second one to print them.
-   Note: we could use only one thanks to seek_in, but seeking on and on in
-   the file we parse seems a bit risky to me.  B.B.  *)
-
-let open_file_twice_if verbosely longfname =
-  let in_chan = open_utf8_file_in longfname in
-  let verb_ch =
-    if verbosely then Some (open_utf8_file_in longfname) else None in
-  let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
-  (in_chan, longfname, (po, verb_ch))
-
-let close_input in_chan (_,verb) =
-  try
-    close_in in_chan;
-    match verb with
-      | Some verb_ch -> close_in verb_ch
-      | _ -> ()
-  with e when CErrors.noncritical e -> ()
-
-let verbose_phrase verbch loc =
-  let loc = Loc.unloc loc in
-  match verbch with
-    | Some ch ->
-	let len = snd loc - fst loc in
-	let s = Bytes.create len in
-        seek_in ch (fst loc);
-        really_input ch s 0 len;
-        Feedback.msg_notice (str (Bytes.to_string s))
-    | None -> ()
-
-exception End_of_input
-
-let parse_sentence = Flags.with_option Flags.we_are_parsing
-  (fun (po, verbch) ->
-  match Pcoq.Gram.entry_parse Pcoq.main_entry po with
-    | Some (loc,_ as com) -> verbose_phrase verbch loc; com
-    | None -> raise End_of_input)
+(* Echo from a buffer based on position.
+   XXX: Should move to utility file. *)
+let vernac_echo loc in_chan = let open Loc in
+  let len = loc.ep - loc.bp in
+  seek_in in_chan loc.bp;
+  Feedback.msg_notice @@ str @@ really_input_string in_chan len
 
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
@@ -184,20 +103,43 @@ let print_cmd_header loc com =
   Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Topfmt.std_ft ()
 
-let rec interp_vernac po chan_beautify checknav (loc,com) =
+let pr_open_cur_subgoals () =
+  try Printer.pr_open_subgoals ()
+  with Proof_global.NoCurrentProof -> Pp.str ""
+
+let rec interp_vernac sid po (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 f
-
-    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
+        load_vernac verbosely sid f
+    | v ->
+      try
+        let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in
+
+        (* Main STM interaction *)
+        if ntip <> `NewTip then
+          anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+        (* Due to bug #5363 we cannot use observe here as we should,
+           it otherwise reveals bugs *)
+        (* Stm.observe nsid; *)
+        Stm.finish ();
+
+        (* We could use a more refined criteria depending on the
+           vernac. For now we imitate the old approach. *)
+        let print_goals = not (!Flags.batch_mode || is_query v) in
+
+        if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+        nsid
+
+      with exn when CErrors.noncritical exn ->
+        ignore(Stm.edit_at sid);
+        raise exn
   in
     try
-      checknav loc com;
-      if !beautify then pr_new_syntax po chan_beautify loc (Some com);
-      (* XXX: This is not 100% correct if called from an IDE context *)
+      (* The -time option is only supported from console-based
+         clients due to the way it prints. *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
@@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) =
       else iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac verbosely file =
+and load_vernac verbosely sid file =
   let chan_beautify =
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
-  let (in_chan, fname, input) = open_file_twice_if verbosely file in
+  let in_chan = open_utf8_file_in file in
+  let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
+  let in_pa   = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in
+  let rsid = ref sid 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 = Flags.silently parse_sentence input in
-      CWarnings.set_current_loc (fst loc_ast);
-      Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast;
-    done
+      let loc, ast = Stm.parse_sentence !rsid in_pa in
+
+      (* Printing of vernacs *)
+      if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
+      Option.iter (vernac_echo loc) in_echo;
+
+      checknav_simple (loc, ast);
+      let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
+      rsid := nsid
+    done;
+    !rsid
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
-    close_input in_chan input;    (* we must close the file first *)
+    close_in in_chan;
+    Option.iter close_in in_echo;
     match e with
-      | End_of_input ->
+      | Stm.End_of_input ->
+          (* Is this called so comments at EOF are printed? *)
           if !beautify then
-            pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None;
+            pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None;
           if !Flags.beautify_file then close_out chan_beautify;
+          !rsid
       | reraise ->
          if !Flags.beautify_file then close_out chan_beautify;
 	 iraise (disable_drop e, info)
@@ -239,7 +194,9 @@ and load_vernac verbosely file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast
+let process_expr sid po loc_ast =
+  checknav_deep loc_ast;
+  interp_vernac sid po loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
@@ -308,7 +265,7 @@ let compile verbosely f =
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
-      let _ = load_vernac verbosely long_f_dot_v in
+      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -328,7 +285,7 @@ let compile verbosely f =
       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 long_f_dot_v in
+      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
       Stm.snapshot_vio ldir long_f_dot_vio;
@@ -347,6 +304,3 @@ let compile v f =
   ignore(CoqworkmgrApi.get 1);
   compile v f;
   CoqworkmgrApi.giveback 1
-
-let () = Hook.set Stm.process_error_hook
-  ExplainErr.process_vernac_interp_error
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 0d9f5871a..e75f8f9e8 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -8,30 +8,16 @@
 
 (** Parsing of vernacular. *)
 
-(** Read a vernac command on the specified input (parse only).
-   Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
-
-val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
- Loc.t * Vernacexpr.vernac_expr
-
 (** Reads and executes vernac commands from a stream. *)
+val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 
-exception End_of_input
+(** [load_vernac echo sid file] Loads [file] on top of [sid], will
+    echo the commands if [echo] is set. *)
+val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
-val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit
+(** Compile a vernac file, (f is assumed without .v suffix) *)
+val compile : bool -> string -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t
 val xml_end_library   : (unit -> unit) Hook.t
-
-(** Load a vernac file, verbosely or not. Errors are annotated with file
-   and location *)
-
-val load_vernac : bool -> string -> unit
-
-
-(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
-
-val compile : bool -> string -> unit
-
-val is_navigation_vernac : Vernacexpr.vernac_expr -> bool