diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 29 | ||||
| -rw-r--r-- | stm/stm.mli | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 10 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 5 |
4 files changed, 29 insertions, 19 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e15b6048ba..2e9bf71e49 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1103,7 +1103,8 @@ module Backtrack : sig val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) - val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when + val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when + val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1161,7 +1162,17 @@ end = struct (* {{{ *) " If your use is intentional, you may want to disable this warning and pass" ^ " the \"-async-proofs-cache force\" option to Coq.")) - let undo_vernac_classifier v = + let back_tactic n (id,_,_,tactic,undo) = + let value = (if tactic then 1 else 0) - undo in + if Int.equal n 0 then `Stop id else `Cont (n-value) + + let get_proof ~doc id = + let open Vernacstate in + match state_of_id ~doc id with + | `Valid (Some vstate) -> Some (Proof_global.proof_of_state vstate.proof) + | _ -> None + + let undo_vernac_classifier v ~doc = if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try @@ -1185,9 +1196,7 @@ end = struct (* {{{ *) oid, VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_,tactic,undo) -> - let value = (if tactic then 1 else 0) - undo in - if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in + let oid = fold_until back_tactic n id in oid, VtLater | VernacUndoTo _ | VernacRestart as e -> @@ -1220,8 +1229,16 @@ end = struct (* {{{ *) CErrors.user_err ~hdr:"undo_vernac_classifier" Pp.(str "Cannot undo") + let get_prev_proof ~doc id = + try + let did = fold_until back_tactic 1 id in + get_proof ~doc did + with Not_found -> None + end (* }}} *) +let get_prev_proof = Backtrack.get_prev_proof + let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = hints := Aux_file.load_aux_file_for file @@ -2785,7 +2802,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) match c with (* Meta *) | VtMeta, _ -> - let id, w = Backtrack.undo_vernac_classifier expr in + let id, w = Backtrack.undo_vernac_classifier expr ~doc in process_back_meta_command ~newtip ~head id x w (* Query *) diff --git a/stm/stm.mli b/stm/stm.mli index 50e7f06095..7f70ea18da 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -110,6 +110,10 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] +(* Returns the proof state before the last tactic that was applied at or before +the specified state. Used to compute proof diffs. *) +val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 6be80d29a5..2170477938 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -42,13 +42,6 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -let classifiers = ref [] -let declare_vernac_classifier - (s : Vernacexpr.extend_name) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -162,6 +155,7 @@ let classify_vernac e = | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ | VernacNameSectionHypSet _ + | VernacDeclareCustomEntry _ | VernacComments _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow @@ -194,7 +188,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try List.assoc s !classifiers l () + try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 45fbfb42af..e82b191418 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -9,17 +9,12 @@ (************************************************************************) open Vernacexpr -open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) val classify_vernac : vernac_control -> vernac_classification -(** Install a vernacular classifier for VernacExtend *) -val declare_vernac_classifier : - Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification |