unified style for new hooks and old hooks

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