diff -r 8142ccd13963 -r 4f777a0e1c8b src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Tue Jul 27 21:55:19 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Tue Jul 27 21:55:39 1999 +0200
@@ -118,11 +118,27 @@
   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
 
 
+(* theory loader actions *)
+
+local
+
+fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
+
+fun trace_action ThyInfo.Update name = tell_pg "this theory is loaded:" name
+  | trace_action ThyInfo.Outdate name = tell_pg "you can unlock the theory" name
+  | trace_action ThyInfo.Remove name = tell_pg "you can unlock the theory" name;
+
+in
+  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
+end;
+
+
 (* init *)
 
 fun init isar =
  (setup_messages ();
   setup_state ();
+  setup_thy_loader ();
   print_mode := [proof_generalN];
   set quick_and_dirty;
   if isar then Isar.sync_main () else ());