diff options
| -rw-r--r-- | stm/stm.ml | 21 | ||||
| -rw-r--r-- | stm/stm.mli | 14 |
2 files changed, 34 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 06bc6e3340..5c83dc48ef 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2682,6 +2682,22 @@ 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 CAst.t -> 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 () @@ -2767,6 +2783,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; let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -3169,7 +3186,8 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = +let add ~doc ~ontop ?newtip verb ({ CAst.loc; v=ast } as last) = + Hook.(get document_edit_notify).add_hook last ontop; let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -3213,6 +3231,7 @@ let query ~doc ~at ~route s = s let edit_at ~doc id = + Hook.(get document_edit_notify).edit_hook id; if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = diff --git a/stm/stm.mli b/stm/stm.mli index 91651e3534..01bedb4fd8 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -297,3 +297,17 @@ 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 CAst.t -> 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 |