# HG changeset patch
# User wenzelm
# Date 1309626531 -7200
# Node ID f57bcfb54808f475a5dee1d5139f36548b99964f
# Parent  9cba66fb109ab57f794619989c19ea066d857612
misc tuning;

diff -r 9cba66fb109a -r f57bcfb54808 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Jul 02 10:37:35 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Jul 02 19:08:51 2011 +0200
@@ -34,10 +34,11 @@
 datatype action = Update | Remove;
 
 local
-  val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
+  val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
-  fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
+  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;
 
 
@@ -135,7 +136,7 @@
 
 (** thy operations **)
 
-(* remove theory *)
+(* main loader actions *)
 
 fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if is_finished name then error (loader_msg "attempt to change finished theory" [name])
@@ -151,6 +152,16 @@
   if known_thy name then remove_thy name
   else ());
 
+fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () =>
+  let
+    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 *)
 
@@ -226,7 +237,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time (deps: deps) text name parent_thys =
+fun load_thy initiators update_time deps text name parent_thys =
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -240,13 +251,7 @@
       |> Present.begin_theory update_time dir uses;
 
     val (theory, present) = Outer_Syntax.load_thy name init pos text;
-
-    val parents = map Context.theory_name parent_thys;
-    fun commit () =
-      NAMED_CRITICAL "Thy_Info" (fn () =>
-       (map get_theory parents;
-        change_thys (new_entry name parents (SOME deps, SOME theory));
-        perform Update name));
+    fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
 
 fun check_deps dir name =
@@ -332,16 +337,12 @@
   let
     val name = Context.theory_name theory;
     val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
-    val parents = map Context.theory_name (Theory.parents_of theory);
     val imports = Thy_Load.imports_of theory;
-    val deps = make_deps master imports;
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
       Output.urgent_message ("Registering theory " ^ quote name);
-      map get_theory parents;
-      change_thys (new_entry name parents (SOME deps, SOME theory));
-      perform Update name))
+      update_thy (make_deps master imports) theory))
   end;