From 8b15eee6125f7f8596f17e9c982fb944a5e3f9be Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 1 Apr 2018 01:15:22 +0200 Subject: [stm] Move VernacBacktrack to the toplevel. This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack. --- intf/vernacexpr.ml | 1 - parsing/g_vernac.ml4 | 2 -- printing/ppvernac.ml | 2 -- stm/stm.ml | 41 +++++------------------------------------ stm/vernac_classifier.ml | 2 +- toplevel/coqloop.ml | 7 +++++++ toplevel/g_toplevel.ml4 | 4 ++++ vernac/vernacentries.ml | 1 - vernac/vernacprop.ml | 1 - 9 files changed, 17 insertions(+), 44 deletions(-) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index dc1110ad8..e029c78e4 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -446,7 +446,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 8543d2b84..1863f3e5f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1065,8 +1065,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 7df0a0c94..9dce65374 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -591,8 +591,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 9a8af3a58..a78323323 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 9ff4e3302..4b99836fd 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 -- cgit v1.2.3