[stm] Port the toplevel to the STM.

- We clean-up `Vernac` and make it use the STM API.

- Now functions in `Vernac` for use in the toplevel and compiler take
  an starting `Stateid.t`.

- Duplicated `Stm.interp` entry point is removed.

- The XML protocol call `interp` is disabled.

16 files changed, 221 insertions, 269 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 30edea7f2..7e7bb9858 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -156,6 +156,19 @@ document type". This allows for a more uniform handling of printing
 
 - A few unused hooks were removed due to cleanups, no clients known.
 
+** Toplevel and Vernacular API **
+
+- The components related to vernacular interpretation have been moved
+  to their own folder `vernac/` whereas toplevel now contains the
+  proper toplevel shell and compiler.
+
+- Coq's toplevel has been ported to directly use the common `Stm`
+  API. The signature of a few functions has changed as a result.
+
+** XML Protocol **
+
+- The legacy `interp` call has been turned into a noop.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 889757764..bc7ce3883 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -8,6 +8,7 @@
 (************************************************************************)
 
 open Vernacexpr
+open Vernacprop
 open CErrors
 open Util
 open Pp
@@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with
   | VernacUnsetOption o -> coqide_known_option o
   | _ -> false
 
-let is_debug cmd = match cmd with
-  | VernacSetOption (["Ltac";"Debug"], _) -> true
-  | _ -> false
-
-let is_query cmd = match cmd with
-  | VernacChdir None
-  | VernacMemOption _
-  | VernacPrintOption _
-  | VernacCheckMayEval _
-  | VernacGlobalCheck _
-  | VernacPrint _
-  | VernacSearch _
-  | VernacLocate _ -> true
-  | _ -> false
-
-let is_undo cmd = match cmd with
-  | VernacUndo _ | VernacUndoTo _ -> true
-  | _ -> false
-
 (** Check whether a command is forbidden in the IDE *)
 
 let ide_cmd_checks (loc,ast) =
@@ -87,7 +69,7 @@ let ide_cmd_checks (loc,ast) =
     user_error "Debug mode not available in the IDE";
   if is_known_option ast then
     Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead");
-  if Vernac.is_navigation_vernac ast || is_undo ast then
+  if is_navigation_vernac ast || is_undo ast then
     Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead");
   if is_query ast then
     Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts")
@@ -132,7 +114,7 @@ let query (s,id) =
 let annotate phrase =
   let (loc, ast) =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
-    Vernac.parse_sentence (pa,None)
+    Stm.parse_sentence (Stm.get_current_state ()) pa
   in
   (* XXX: Width should be a parameter of annotate... *)
   Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
@@ -394,26 +376,9 @@ let init =
          initial_id
    end
 
-(* Retrocompatibility stuff *)
+(* Retrocompatibility stuff, disabled since 8.7 *)
 let interp ((_raw, verbose), s) =
-  let vernac_parse s =
-    let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-    Flags.with_option Flags.we_are_parsing (fun () ->
-      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
-      | None -> raise (Invalid_argument "vernac_parse")
-      | Some ast -> ast)
-    () in
-  Stm.interp verbose (vernac_parse s);
-  (* TODO: the "" parameter is a leftover of the times the protocol
-   * used to include stderr/stdout output.
-   *
-   * Currently, we force all the output meant for the to go via the
-   * feedback mechanism, and we don't manipulate stderr/stdout, which
-   * are left to the client's discrection. The parameter is still there
-   * as not to break the core protocol for this minor change, but it should
-   * be removed in the next version of the protocol.
-   *)
-  Stm.get_current_state (), CSig.Inl ""
+  Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add."
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
diff --git a/lib/flags.ml b/lib/flags.ml
index 5b080151c..ef5eddfb2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,8 +86,6 @@ let in_toplevel = ref false
 let profile = false
 
 let print_emacs = ref false
-let coqtop_ui = ref false
-
 let xml_export = ref false
 
 let ide_slave = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index bd365e653..f5e1c96f9 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -46,9 +46,8 @@ val in_toplevel : bool ref
 
 val profile : bool
 
+(* Legacy flags *)
 val print_emacs : bool ref
-val coqtop_ui : bool ref
-
 val xml_export : bool ref
 
 val ide_slave : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index fb0a0514d..8d212a6a0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -323,6 +323,15 @@ end = struct (* {{{ *)
   open Printf
 
   let print_dag vcs () =
+
+    (* Due to threading, be wary that this will be called from the
+       toplevel with we_are_parsing set to true, as indeed, the
+       toplevel is waiting for input . What a race! XD
+
+       In case you are hitting the race enable stm_debug.
+    *)
+    if stm_debug then Flags.we_are_parsing := false;
+
     let fname =
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
     let string_of_transaction = function
@@ -970,7 +979,6 @@ module Backtrack : sig
 
   val record : unit -> unit
   val backto : Stateid.t -> unit
-  val back_safe : unit -> unit
 
   (* we could navigate the dag, but this ways easy *)
   val branches_of : Stateid.t -> backup
@@ -2342,22 +2350,18 @@ let observe id =
     VCS.restore vcs;
     iraise e
 
-let pr_open_cur_subgoals () =
-  try Printer.pr_open_subgoals ()
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
-let finish ?(print_goals=false) () =
+let finish () =
   let head = VCS.current_branch () in
   observe (VCS.get_branch_pos head);
-  if print_goals then msg_notice (pr_open_cur_subgoals ());
   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
   | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
   | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
   | _ -> ()
 
-
 let wait () =
   Slaves.wait_all_done ();
   VCS.print ()
@@ -2435,29 +2439,17 @@ let merge_proof_branch ~valid ?id qast keep brname =
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
-let handle_failure (e, info) vcs tty =
+let handle_failure (e, info) vcs =
   if e = CErrors.Drop then iraise (e, info) else
   match Stateid.get info with
   | None ->
       VCS.restore vcs;
       VCS.print ();
-      if tty && interactive () = `Yes then begin
-        (* Hopefully the 1 to last state is valid *)
-        Backtrack.back_safe (); 
-        VCS.checkout_shallowest_proof_branch ();
-      end;
-      VCS.print ();
       anomaly(str"error with no safe_id attached:" ++ spc() ++
         CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
       stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
-      if tty && interactive () = `Yes then begin
-        (* We stay on a valid state *)
-        Backtrack.backto safe_id;
-        VCS.checkout_shallowest_proof_branch ();
-        Reach.known_state ~cache:(interactive ()) safe_id;
-      end;
       VCS.print ();
       iraise (e, info)
 
@@ -2471,7 +2463,7 @@ let snapshot_vio ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+let process_transaction ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
@@ -2517,13 +2509,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
       (* Query *)
-      | VtQuery (false,(report_id,route)), VtNow when tty = true ->
-          finish ();
-          (try Future.purify (stm_vernac_interp report_id ~route)
-            {x with verbose = true }
-           with e when CErrors.noncritical e ->
-             let e = CErrors.push e in
-             iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
       | VtQuery (false,(report_id,route)), VtNow ->
           (try stm_vernac_interp report_id ~route x
            with e ->
@@ -2655,7 +2640,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
     rc
   with e ->
     let e = CErrors.push e in
-    handle_failure e vcs tty
+    handle_failure e vcs
 
 let get_ast id =
   match VCS.visit id with
@@ -2743,7 +2728,7 @@ let add ~ontop ?newtip verb (loc, ast) =
   (* XXX: Classifiy vernac should be moved inside process transaction *)
   let clas = classify_vernac ast in
   let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
-  match process_transaction ?newtip ~tty:false aast clas with
+  match process_transaction ?newtip aast clas with
   | `Ok -> VCS.cur_tip (), `NewTip
   | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
 
@@ -2766,10 +2751,9 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
     | VtStm (w,_), _ ->
-       ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
+       ignore(process_transaction aast (VtStm (w,false), VtNow))
     | _ ->
-       ignore(process_transaction
-         ~tty:false aast (VtQuery (false,report_with), VtNow)))
+       ignore(process_transaction aast (VtQuery (false,report_with), VtNow)))
   s
 
 let edit_at id =
@@ -2898,32 +2882,11 @@ let edit_at id =
 let backup () = VCS.backup ()
 let restore d = VCS.restore d
 
+let get_current_state () = VCS.cur_tip ()
+
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
-let interp verb (loc,e) =
-  let clas = classify_vernac e in
-  let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
-  let rc = process_transaction ~tty:true aast clas in
-  if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
-  if interactive () = `Yes ||
-     (!Flags.async_proofs_mode = Flags.APoff &&
-      !Flags.compilation_mode = Flags.BuildVo) then
-    let vcs = VCS.backup () in
-    let print_goals =
-      verb && match clas with
-       | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
-       | _ -> not !Flags.coqtop_ui in
-    try finish ~print_goals ()
-    with e ->
-      let e = CErrors.push e in
-      handle_failure e vcs true
-
-let finish () = finish ()
-
-let get_current_state () = VCS.cur_tip ()
-
 let current_proof_depth () =
   let head = VCS.current_branch () in
   match VCS.get_branch head with
diff --git a/stm/stm.mli b/stm/stm.mli
index a31e4289d..30e9629c6 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -30,7 +30,7 @@ exception End_of_input
    If [newtip] is provided, then the returned state id is guaranteed
    to be [newtip] *)
 val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
-  bool -> (Loc.t * Vernacexpr.vernac_expr) ->
+  bool -> Vernacexpr.vernac_expr Loc.located ->
   Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
@@ -205,13 +205,6 @@ type state = {
 val state_of_id :
   Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 
-(** read-eval-print loop compatible interface ****************************** **)
-
-(* Adds a new line to the document.  It replaces the core of Vernac.interp.
-   [finish] is called as the last bit of this function if the system
-   is running interactively (-emacs or coqtop). *)
-val interp : bool -> vernac_expr located -> unit
-
 (* Queries for backward compatibility *)
 val current_proof_depth : unit -> int
 val get_all_proof_names : unit -> Id.t list
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..17d8f5f49 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -257,7 +257,7 @@ 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
@@ -271,13 +271,11 @@ let rec discard_to_dot () =
     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 ();
@@ -312,25 +310,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()));
   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.
@@ -349,10 +346,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 4968804fd..c8f3ca1ab 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -175,15 +175,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
@@ -641,8 +641,9 @@ let init_toplevel arglist =
       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 d5ceeaccd..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;
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
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 283c095eb..d631fae8a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,3 +1,4 @@
+Vernacprop
 Lemmas
 Himsg
 ExplainErr
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
new file mode 100644
index 000000000..ec78d6012
--- /dev/null
+++ b/vernac/vernacprop.ml
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* We define some high-level properties of vernacular commands, used
+   mainly by the UI components *)
+
+open Vernacexpr
+
+(* 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 is_debug cmd = match cmd with
+  | VernacSetOption (["Ltac";"Debug"], _) -> true
+  | _ -> false
+
+let is_query cmd = match cmd with
+  | VernacChdir None
+  | VernacMemOption _
+  | VernacPrintOption _
+  | VernacCheckMayEval _
+  | VernacGlobalCheck _
+  | VernacPrint _
+  | VernacSearch _
+  | VernacLocate _ -> true
+  | _ -> false
+
+let is_undo cmd = match cmd with
+  | VernacUndo _ | VernacUndoTo _ -> true
+  | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
new file mode 100644
index 000000000..c235ecfb5
--- /dev/null
+++ b/vernac/vernacprop.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* We define some high-level properties of vernacular commands, used
+   mainly by the UI components *)
+
+open Vernacexpr
+
+val is_navigation_vernac : vernac_expr -> bool
+val is_deep_navigation_vernac : vernac_expr -> bool
+val is_reset : vernac_expr -> bool
+val is_query : vernac_expr -> bool
+val is_debug : vernac_expr -> bool
+val is_undo : vernac_expr -> bool