[wp] removed nodes callbacks

src/plugins/server/data.ml

@@ -593,6 +593,7 @@ sig
   val empty : 'a t
   val add : key -> 'a -> 'a t -> 'a t
   val find : key -> 'a t -> 'a
+  val remove : key -> 'a t -> 'a t
 end
 
 module type Index =
@@ -601,6 +602,7 @@ sig
   type tag
   val get : t -> tag
   val find : tag -> t
+  val remove : t -> unit
   val clear : unit -> unit
 end
 
@@ -611,6 +613,7 @@ sig
   val clear : index -> unit
   val get : index -> M.key -> int
   val find : index -> int -> M.key
+  val remove : index -> M.key -> unit
   val to_json : index -> M.key -> json
   val of_json : index -> json -> M.key
 end =
@@ -643,6 +646,13 @@ struct
       m.index <- M.add a id m.index ;
       Hashtbl.add m.lookup id a ; id
 
+  let remove m a =
+    try
+      let id = M.find a m.index in
+      Hashtbl.remove m.lookup id ;
+      m.index <- M.remove a m.index ;
+    with Not_found -> ()
+
   let find m id = Hashtbl.find m.lookup id
 
   let to_json m a = `Int (get m a)
@@ -662,6 +672,7 @@ struct
   let clear () = INDEX.clear index
   let get = INDEX.get index
   let find = INDEX.find index
+  let remove = INDEX.remove index
   include
     (struct
       type t = M.key
@@ -694,6 +705,7 @@ struct
 
   let index () = STATE.get ()
   let clear () = INDEX.clear (index())
+  let remove a = INDEX.remove (index()) a
 
   let get a = INDEX.get (index()) a
   let find id = INDEX.find (index()) id
@@ -761,6 +773,11 @@ struct
     let hash = lookup () in
     if not (Hashtbl.mem hash tag) then Hashtbl.add hash tag x ; tag
 
+  let remove x =
+    let tag = A.id x in
+    let hash = lookup () in
+    Hashtbl.remove hash tag
+
   include
     (struct
       type t = A.t

src/plugins/server/data.mli

@@ -357,6 +357,7 @@ sig
   val empty : 'a t
   val add : key -> 'a -> 'a t -> 'a t
   val find : key -> 'a t -> 'a
+  val remove : key -> 'a t -> 'a t
 end
 
 (** Datatype extended with access to value identifiers. *)
@@ -368,6 +369,9 @@ sig
   val find : tag -> t
   (** @raise Not_found if not registered. *)
 
+  val remove : t -> unit
+  (** Remove item from index tables. Use with extreme care. *)
+
   val clear : unit -> unit
   (** Clear index tables. Use with extreme care. *)
 end

src/plugins/wp/ProofEngine.ml

@@ -113,6 +113,12 @@ let set_saved t s = t.saved <- s
 (* --- Removal                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
+let clear_hooks = ref []
+let remove_hooks = ref []
+
+let add_clear_hook fn = clear_hooks := !clear_hooks @ [fn]
+let add_remove_hook fn = remove_hooks := !remove_hooks @ [fn]
+
 let rec revert_tactic t n =
   n.strategy <- None ;
   match n.script with
@@ -125,15 +131,13 @@ and remove_node t n =
     Wpo.remove n.goal
   else
     Wpo.clear_results n.goal ;
-  begin
-    match t.head with
-    | Some n0 when n0 == n -> t.head <- None
-    | _ -> ()
-  end ;
+  List.iter (fun f -> f n) !remove_hooks ;
+  Option.iter (fun n0 -> if n0 == n then t.head <- None) t.head ;
   revert_tactic t n
 
 let clear_tree t =
   begin
+    List.iter (fun f -> f ()) !clear_hooks ;
     Wpo.clear_results t.main ;
     Option.iter (remove_node t) t.root ;
     t.gid <- 0 ;

src/plugins/wp/ProofEngine.mli

@@ -101,6 +101,8 @@ val clear_tree : tree -> unit
 val clear_node : tree -> node -> unit
 val clear_node_tactic : tree -> node -> unit
 val clear_parent_tactic : tree -> node -> unit
+val add_clear_hook : (unit -> unit) -> unit
+val add_remove_hook : (node -> unit) -> unit
 
 val cancel_parent_tactic : tree -> unit
 val cancel_current_node : tree -> unit

src/plugins/wp/wpTipApi.ml

@@ -59,6 +59,12 @@ module Node = D.Index
       let descr = Md.plain "Proof Node index"
     end)
 
+let () = Server.Main.once
+    begin fun () ->
+      ProofEngine.add_clear_hook Node.clear ;
+      ProofEngine.add_remove_hook Node.remove ;
+    end
+
 module Tactic : D.S with type t = Tactical.t =
 struct
   type t = Tactical.t