diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 31 | ||||
| -rw-r--r-- | stm/stm.mli | 10 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 17 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 5 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 16 |
5 files changed, 35 insertions, 44 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 0aed88a53f..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 *) @@ -2976,7 +2993,7 @@ let parse_sentence ~doc sid pa = str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur."); Flags.with_option Flags.we_are_parsing (fun () -> try - match Pcoq.Gram.entry_parse Pvernac.main_entry pa with + match Pcoq.Entry.parse Pvernac.main_entry pa with | None -> raise End_of_input | Some (loc, cmd) -> CAst.make ~loc cmd with e when CErrors.noncritical e -> diff --git a/stm/stm.mli b/stm/stm.mli index aed7274d06..7f70ea18da 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -92,11 +92,11 @@ val new_doc : stm_init_options -> doc * Stateid.t (** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> +val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using - [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) + [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) exception End_of_input @@ -110,11 +110,15 @@ 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 *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e01dcbcb6e..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,16 +188,13 @@ 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 | VernacExpr (f, e) -> - let poly = List.fold_left (fun poly f -> - match f with - | VernacPolymorphic b -> b - | (VernacProgram | VernacLocal _) -> poly - ) poly f in + let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in + let poly = atts.Vernacinterp.polymorphic in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> 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 diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli deleted file mode 100644 index 37ec6dacca..0000000000 --- a/stm/workerLoop.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Default priority *) -val async_proofs_worker_priority : CoqworkmgrApi.priority ref - -val loop : - (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> - Coqargs.coq_cmdopts * string list |