diff options
| -rw-r--r-- | CREDITS | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 34 | ||||
| -rw-r--r-- | stm/stm.mli | 25 |
3 files changed, 27 insertions, 33 deletions
@@ -170,6 +170,7 @@ of the Coq Proof assistant during the indicated time: Nickolai Zeldovich (MIT 2014-2016) Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806, INRIA-PPS then IRIF, 2015-now) + Talia Ringer (UW, 2019) *************************************************************************** INRIA refers to: diff --git a/stm/stm.ml b/stm/stm.ml index 648d2de807..10f4865dfd 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) *) @@ -2682,22 +2691,6 @@ let doc_type_module_name (std : stm_doc_type) = | Interactive mn -> Names.DirPath.to_string mn *) -(* Document edit notifiers *) -type document_edit_notifiers = - { add_hook : Vernacexpr.vernac_control -> Stateid.t -> unit - (** User adds a sentence to the document (after parsing) *) - ; edit_hook : Stateid.t -> unit - (** User edits a sentence in the document *) - ; exec_hook : Stateid.t -> unit - (** User requests checking of a sentence in the document. *) - } - -(** Set the document edit notifiers. *) -let document_edit_notify, document_edit_hook = - Hook.make ~default:{ add_hook = (fun _ _ -> ()) - ; edit_hook = (fun _ -> ()) - ; exec_hook = (fun _ -> ()) } () - let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () @@ -2783,7 +2776,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = doc, VCS.cur_tip () let observe ~doc id = - Hook.(get document_edit_notify).exec_hook id; + Hooks.(call sentence_exec id); let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -3139,7 +3132,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> ) (0, 0) loc let add ~doc ~ontop ?newtip verb ast = - Hook.(get document_edit_notify).add_hook ast ontop; + 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 @@ -3185,7 +3178,7 @@ let query ~doc ~at ~route s = s let edit_at ~doc id = - Hook.(get document_edit_notify).edit_hook 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 = @@ -3341,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 06d3d28057..9cf5206cfa 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -282,6 +282,17 @@ 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 -> @@ -297,17 +308,3 @@ val stm_debug : bool ref type document val backup : unit -> document val restore : document -> unit - -(** Experimental Hooks for UI experiment plugins, not for general use! *) - -type document_edit_notifiers = - { add_hook : Vernacexpr.vernac_control -> Stateid.t -> unit - (** User adds a sentence to the document (after parsing) *) - ; edit_hook : Stateid.t -> unit - (** User edits a sentence in the document *) - ; exec_hook : Stateid.t -> unit - (** User requests checking of a sentence in the document. *) - } - -(** Set the document edit notifiers. *) -val document_edit_hook : document_edit_notifiers Hook.t |