# HG changeset patch
# User wenzelm
# Date 1419265020 -3600
# Node ID f96ff29aa00cb6a939607c409a2bf06d8f162f3f
# Parent  8cf1bad1c2e7b1a58f72c1c3941b603f38b9213d
removed remains from Proof General;

diff -r 8cf1bad1c2e7 -r f96ff29aa00c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Dec 22 16:44:54 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Dec 22 17:17:00 2014 +0100
@@ -7,8 +7,6 @@
 
 signature THY_INFO =
 sig
-  datatype action = Update | Remove
-  val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
@@ -29,20 +27,6 @@
 structure Thy_Info: THY_INFO =
 struct
 
-(** theory loader actions and hooks **)
-
-datatype action = Update | Remove;
-
-local
-  val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
-in
-  fun add_hook f = Synchronized.change hooks (cons f);
-  fun perform action name =
-    List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks);
-end;
-
-
-
 (** thy database **)
 
 (* messages *)
@@ -136,7 +120,6 @@
     let
       val succs = thy_graph String_Graph.all_succs [name];
       val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
-      val _ = List.app (perform Remove) succs;
       val _ = change_thys (fold String_Graph.del_node succs);
     in () end);
 
@@ -151,7 +134,6 @@
     val _ = kill_thy name;
     val _ = map get_theory parents;
     val _ = change_thys (new_entry name parents (SOME deps, SOME theory));
-    val _ = perform Update name;
   in () end);