[stm] Add hooks for document actions.

This arose after a question by Talia Ringer on how to log
user-interaction with a Coq document.

The hooks would allow a plugin to receive events about user data.

This is experimental and will need some tweaks to be useful for sure,
in particular w.r.t. errors.

[Note: this is safe enough as to be included in 8.9]

1 files changed, 14 insertions, 0 deletions

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