Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.

9 files changed, 17 insertions, 44 deletions

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 96b4a0e26..0e84a07aa 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -442,7 +442,6 @@ type nonrec vernac_expr =
   | VernacRestart
   | VernacUndo of int
   | VernacUndoTo of int
-  | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus
   | VernacUnfocused
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7114e6c58..8b445985b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1037,8 +1037,6 @@ GEXTEND Gram
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
       | IDENT "BackTo"; n = natural -> VernacBackTo n
-      | IDENT "Backtrack"; n = natural ; m = natural ; p = natural ->
-	  VernacBacktrack (n,m,p)
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2706893ac..bbf0e2b60 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -584,8 +584,6 @@ open Decl_kinds
         )
       | VernacUndoTo i ->
         return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
-      | VernacBacktrack (i,j,k) ->
-        return (keyword "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k])
       | VernacFocus i ->
         return (keyword "Focus" ++ pr_opt int i)
       | VernacShow s ->
diff --git a/stm/stm.ml b/stm/stm.ml
index e970a02ee..a0305efee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1072,7 +1072,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
   let is_filtered_command = function
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
-    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+    | VernacAbortAll | VernacAbort _ -> true
     | _ -> false
   in
   let aux_interp st expr =
@@ -1097,7 +1097,6 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
 module Backtrack : sig
 
   val record : unit -> unit
-  val backto : Stateid.t -> unit
 
   (* we could navigate the dag, but this ways easy *)
   val branches_of : Stateid.t -> backup
@@ -1122,14 +1121,6 @@ end = struct (* {{{ *)
       info.vcs_backup <- backup, branches)
     [VCS.current_branch (); VCS.Branch.master]
 
-  let backto oid =
-    let info = VCS.get_info oid in
-    match info.vcs_backup with
-    | None, _ ->
-       anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++
-               str": a state with no vcs_backup.")
-    | Some vcs, _ -> VCS.restore vcs
-
   let branches_of id =
     let info = VCS.get_info id in
     match info.vcs_backup with
@@ -1220,7 +1211,6 @@ end = struct (* {{{ *)
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           oid, VtLater
-      | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
           Stateid.of_int id, VtNow
       | _ -> anomaly Pp.(str "incorrect VtMeta classification")
@@ -2757,9 +2747,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
-  match part_of_script, w with
-  | true, w ->
+let process_back_meta_command ~newtip ~head oid aast w =
     let id = VCS.new_node ~id:newtip () in
     let { mine; others } = Backtrack.branches_of oid in
     let valid = VCS.get_branch_pos head in
@@ -2779,16 +2767,7 @@ let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
     VCS.commit id (Alias (oid,aast));
     Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-  | false, VtNow ->
-    stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid);
-    Backtrack.backto oid;
-    VCS.checkout_shallowest_proof_branch ();
-    Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok
-
-  | false, VtLater ->
-    anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.")
-
-let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
+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
@@ -2802,12 +2781,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       (* Meta *)
       | VtMeta, _ ->
         let id, w = Backtrack.undo_vernac_classifier expr in
-        (* Special case Backtrack, as it is never part of a script. See #6240 *)
-        let part_of_script = begin match Vernacprop.under_control expr with
-          | VernacBacktrack _ -> false
-          | _ -> part_of_script
-        end in
-        process_back_meta_command ~part_of_script ~newtip ~head id x w
+        process_back_meta_command ~newtip ~head id x w
       (* Query *)
       | VtQuery (false,route), VtNow ->
         let query_sid = VCS.cur_tip () in
@@ -3074,13 +3048,8 @@ let query ~doc ~at ~route s =
         let { CAst.loc; v=ast } = parse_sentence ~doc at s in
         let indentation, strlen = compute_indentation ?loc at in
         CWarnings.set_current_loc loc;
-        let clas = Vernac_classifier.classify_vernac ast in
         let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
-        match clas with
-        | VtMeta , _ -> (* TODO: can this still happen ? *)
-          ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
-        | _ ->
-          ignore(process_transaction aast (VtQuery (false,route), VtNow))
+        ignore(process_transaction aast (VtQuery (false,route), VtNow))
       done;
     with
     | End_of_input -> ()
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4efe1f7ba..eecee40df 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -183,7 +183,7 @@ let classify_vernac e =
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+    | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
     (* What are these? *)
     | VernacRestoreState _
     | VernacWriteState _ -> VtSideff [], VtNow
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 64d839f18..371be20d2 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -338,6 +338,13 @@ let rec vernac_loop ~state =
   try
     let input = top_buffer.tokens in
     match read_sentence ~state input with
+    | {v=VernacBacktrack(bid,_,_)} ->
+      let bid = Stateid.of_int bid in
+      let doc, res = Stm.edit_at ~doc:state.doc bid in
+      assert (res = `NewTip);
+      let state = { state with doc; sid = bid } in
+      vernac_loop ~state
+
     | {v=VernacQuit} ->
       exit 0
     | {v=VernacDrop} ->
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
index 7526f3071..d5d558b9b 100644
--- a/toplevel/g_toplevel.ml4
+++ b/toplevel/g_toplevel.ml4
@@ -9,10 +9,12 @@
 (************************************************************************)
 
 open Pcoq
+open Pcoq.Prim
 open Vernacexpr
 
 (* Vernaculars specific to the toplevel *)
 type vernac_toplevel =
+  | VernacBacktrack of int * int * int
   | VernacDrop
   | VernacQuit
   | VernacControl of vernac_control
@@ -31,6 +33,8 @@ GEXTEND Gram
   vernac_toplevel: FIRST
     [ [ IDENT "Drop"; "." -> CAst.make VernacDrop
       | IDENT "Quit"; "." -> CAst.make VernacQuit
+      | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
+        CAst.make (VernacBacktrack (n,m,p))
       | cmd = main_entry ->
               match cmd with
               | None -> raise Stm.End_of_input
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5dcc170b1..0e8ca2289 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2008,7 +2008,6 @@ let interp ?proof ~atts ~st c =
   | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
   | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
   | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
-  | VernacBacktrack _ -> CErrors.user_err  (str "Backtrack cannot be used through the Load command")
 
   (* Resetting *)
   | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index a837b77a3..0fdd2faaf 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -31,7 +31,6 @@ let rec has_Fail = function
 let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
-  | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
   | _ -> false