Merge PR #8768: [stm] Add hooks for document actions.

Reviewed-by: gares

3 files changed, 29 insertions, 0 deletions

diff --git a/CREDITS b/CREDITS
index f871dba8b3..9b5c1507f5 100644
--- a/CREDITS
+++ b/CREDITS
@@ -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 6f7cefb582..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) *)
@@ -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 ->