From 7eefc0b1db614158ed1b322f8c6e5601e3995113 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Oct 2018 23:19:50 +0200
Subject: [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]
---
 stm/stm.ml  | 21 ++++++++++++++++++++-
 stm/stm.mli | 14 ++++++++++++++
 2 files changed, 34 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 7ea5bd0c7180b21e03f6118b3534b3b2f0792758 Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Wed, 22 May 2019 17:29:29 -0400
Subject: unified style for new hooks and old hooks

---
 CREDITS     |  1 +
 stm/stm.ml  | 34 +++++++++++++++-------------------
 stm/stm.mli | 25 +++++++++++--------------
 3 files changed, 27 insertions(+), 33 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 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
-- 
cgit v1.2.3


From 4757e4f20680c320ac9657b1a6d1570071269850 Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Wed, 22 May 2019 18:06:50 -0400
Subject: Fix ambiguous comment problem

---
 stm/stm.mli | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stm/stm.mli b/stm/stm.mli
index 9cf5206cfa..a0bbe05b3a 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -288,8 +288,10 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
 
 (** 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
 
-- 
cgit v1.2.3