diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 17 | ||||
| -rw-r--r-- | stm/stm.mli | 13 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
3 files changed, 31 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 6f7cefb582..fc539b5208 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -100,6 +100,15 @@ let forward_feedback, forward_feedback_hook = let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () +let document_add, document_add_hook = Hook.make + ~default:(fun _ _ -> ()) () + +let document_edit, document_edit_hook = Hook.make + ~default:(fun _ -> ()) () + +let sentence_exec, sentence_exec_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) @@ -571,7 +580,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i - | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i + | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -2767,6 +2776,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = doc, VCS.cur_tip () let observe ~doc id = + Hooks.(call sentence_exec id); let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -3122,6 +3132,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> ) (0, 0) loc let add ~doc ~ontop ?newtip verb ast = + Hooks.(call document_add ast ontop); let loc = ast.CAst.loc in let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then @@ -3167,6 +3178,7 @@ let query ~doc ~at ~route s = s let edit_at ~doc id = + Hooks.(call document_edit id); if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = @@ -3322,6 +3334,9 @@ let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_hook +let document_add_hook = Hooks.document_add_hook +let document_edit_hook = Hooks.document_edit_hook +let sentence_exec_hook = Hooks.sentence_exec_hook let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs diff --git a/stm/stm.mli b/stm/stm.mli index 9d2bf56629..a0bbe05b3a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -282,6 +282,19 @@ val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t +(* + * Hooks into the UI for plugins (not for general use) + *) + +(** User adds a sentence to the document (after parsing) *) +val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t + +(** User edits a sentence in the document *) +val document_edit_hook : (Stateid.t -> unit) Hook.t + +(** User requests evaluation of a sentence *) +val sentence_exec_hook : (Stateid.t -> unit) Hook.t + val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 7cecd801e4..aa16f9535d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -188,11 +188,11 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater - | VernacInstance (_,((name,_),_,_),_,_) -> + | VernacInstance ((name,_),_,_,_,_) -> VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll |