src/Pure/Thy/thy_info.ML

   val use_thy: string -> unit
   val update_thy: string -> unit
   val remove_thy: string -> unit
   val time_use_thy: string -> unit
   val use_thy_only: string -> unit
+  val update_thy_only: string -> unit
 end;
 
 signature THY_INFO =
 sig
   include BASIC_THY_INFO
+  datatype action = Update | Outdate | Remove
+  val str_of_action: action -> string
+  val add_hook: (action -> string -> unit) -> unit
   val names: unit -> string list
   val get_theory: string -> theory
-  val put_theory: theory -> unit
   val get_preds: string -> string list
   val loaded_files: string -> (Path.T * File.info) list
+  val touch_all_thys: unit -> unit
   val load_file: bool -> Path.T -> unit
   val use_path: Path.T -> unit
   val use: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory
   val end_theory: theory -> theory

 
 structure ThyInfo: THY_INFO =
 struct
 
 
+(** theory loader actions and hooks **)
+
+datatype action = Update | Outdate | Remove;
+val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
+
+local
+  val hooks = ref ([]: (action -> string -> unit) list);
+in
+  fun add_hook f = hooks := f :: ! hooks;
+  fun perform action name = seq (fn f => f action name) (! hooks);
+end;
+
+
+
 (** thy database **)
 
 (* messages *)
 
 fun gen_msg txt [] = txt

   | _ => error (loader_msg "undefined theory entry for" [name]));
 
 val theory_of_sign = get_theory o Sign.name_of;
 val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
 
-fun put_theory theory =
-  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory));
+fun put_theory name theory = change_thy name (fn (deps, _) => (deps, Some theory));
 
 
 
 (** thy operations **)
 
 (* maintain 'outdated' flag *)
+
+local
 
 fun is_outdated name =
   (case lookup_deps name of
     Some (Some {outdated, ...}) => outdated
   | _ => false);
 
 fun outdate_thy name =
-  if is_finished name then ()
-  else change_deps name (apsome (fn {present, outdated = _, master, files} =>
-    make_deps present true master files));
+  if is_finished name orelse is_outdated name then ()
+  else (change_deps name (apsome (fn {present, outdated = _, master, files} =>
+    make_deps present true master files)); perform Outdate name);
+
+in
 
 fun touch_thy name =
-  if is_outdated name then ()
-  else if is_finished name then warning (loader_msg "tried to touch finished theory" [name])
-  else
-    (case filter_out is_outdated (thy_graph Graph.all_succs [name]) \ name of
-      [] => outdate_thy name
-    | names =>
-       (warning (loader_msg "the following theories become out-of-date:" names);
-        seq outdate_thy names; outdate_thy name));
-
-val untouch_deps = apsome (fn {present, outdated = _, master, files}: deps =>
-  make_deps present false master files);
-
-
-(* load_thy *)
-
-fun required_by [] = ""
-  | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
-
-fun load_thy ml time initiators dir name parents =
-  let
-    val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
-    val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
-
-    val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
-    val master = ThyLoad.load_thy dir name ml time;
-
-    val files = get_files name;
-    val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
-  in
-    if null missing_files then ()
-    else warning (loader_msg "unresolved dependencies of theory" [name] ^
-      "\nfile(s): " ^ commas_quote missing_files);
-    change_deps name (fn _ => Some (make_deps true false master files))
-  end;
+  if is_finished name then warning (loader_msg "tried to touch finished theory" [name])
+  else seq outdate_thy (thy_graph Graph.all_succs [name]);
+
+fun touch_all_thys () = seq outdate_thy (get_names ());
+
+end;
 
 
 (* load_file *)
 
 fun run_file path =

 val use_path = load_file false;
 val use = use_path o Path.unpack;
 val time_use = load_file true o Path.unpack;
 
 
+(* load_thy *)
+
+fun required_by [] = ""
+  | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
+
+fun load_thy ml time initiators dir name parents =
+  let
+    val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
+    val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
+
+    val _ = touch_thy name;
+    val master = ThyLoad.load_thy dir name ml time;
+
+    val files = get_files name;
+    val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
+  in
+    if null missing_files then ()
+    else warning (loader_msg "unresolved dependencies of theory" [name] ^
+      "\nfile(s): " ^ commas_quote missing_files);
+    change_deps name (fn _ => Some (make_deps true false master files));
+    perform Update name
+  end;
+
+
 (* require_thy *)
 
-fun init_deps master files = Some (make_deps false false master (map (rpair None) files));
+fun init_deps master files = Some (make_deps false true master (map (rpair None) files));
 
 fun load_deps dir name ml =
   let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml
   in (Some (init_deps master files), parents) end;
 

         val dir = Path.append prfx (Path.dir path);
         val req_parent =
           require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
 
         val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
-          error (loader_msg "The error(s) above occurred while examining theory" [name] ^
+          error (loader_msg "the error(s) above occurred while examining theory" [name] ^
             (if null initiators then "" else "\n" ^ required_by initiators));
         val (visited', parent_results) = foldl_map req_parent (name :: visited, parents);
 
         val result =
           if current andalso forall #1 parent_results then true
           else
             ((case new_deps of
-              Some deps => change_thys (update_node name parents (untouch_deps deps, None))
+              Some deps => change_thys (update_node name parents (deps, None))
             | None => ());
-              load_thy ml time initiators dir name parents;
-              false);
+             load_thy ml time initiators dir name parents;
+             false);
       in (visited', (result, name)) end
   end;
 
 fun gen_use_thy req s =
   let val (_, (_, name)) = req [] Path.current ([], s)
   in Context.context (get_theory name) end;
 
-val weak_use_thy = gen_use_thy (require_thy true false false false);
-val use_thy      = gen_use_thy (require_thy true false true false);
-val update_thy   = gen_use_thy (require_thy true false true true);
-val time_use_thy = gen_use_thy (require_thy true true true false);
-val use_thy_only = gen_use_thy (require_thy false false true false);
+val weak_use_thy    = gen_use_thy (require_thy true false false false);
+val use_thy         = gen_use_thy (require_thy true false true false);
+val time_use_thy    = gen_use_thy (require_thy true true true false);
+val use_thy_only    = gen_use_thy (require_thy false false true false);
+val update_thy      = gen_use_thy (require_thy true false true true);
+val update_thy_only = gen_use_thy (require_thy false false true true);
 
 
 (* remove_thy *)
 
 fun remove_thy name =
   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   else
     let val succs = thy_graph Graph.all_succs [name] in
       writeln (loader_msg "removing" succs);
-      change_thys (Graph.del_nodes succs)
+      change_thys (Graph.del_nodes succs);
+      seq (perform Remove) succs
     end;
 
 
 (* begin / end theory *)
 

     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
 
 fun end_theory theory =
-  let val theory' = PureThy.end_theory theory
-  in put_theory theory'; theory' end;
+  let
+    val theory' = PureThy.end_theory theory;
+    val name = PureThy.get_name theory;
+  in put_theory name theory'; theory' end;
 
 
 (* finish all theories *)
 
 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (None, entry)));

         handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
       |> add_deps name parent_names;
   in
     if not (null nonfinished) then err "non-finished parent theories" nonfinished
     else if not (null variants) then err "different versions of parent theories" variants
-    else change_thys register
+    else (change_thys register; perform Update name)
   end;
 
 
 (*final declarations of this structure*)
 val theory = get_theory;