src/Pure/Thy/thy_info.ML

 file dependencies.
 *)
 
 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
   val is_finished: string -> bool
   val master_directory: string -> Path.T

 end;
 
 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 *)
 
 val show_path = space_implode " via " o map quote;

   if is_finished name then error ("Cannot update finished theory " ^ quote name)
   else
     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);
 
 fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if known_thy name then remove_thy name

     val name = Context.theory_name theory;
     val parents = map Context.theory_name (Theory.parents_of theory);
     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);
 
 
 (* scheduling loader tasks *)