src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -57,7 +57,7 @@
 local
   val hooks = ref ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = hooks := f :: ! hooks;
+  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
   fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
 end;
 
@@ -122,7 +122,7 @@
   val database = ref (Graph.empty: thy Graph.T);
 in
   fun get_thys () = ! database;
-  val change_thys = Library.change database;
+  fun change_thys f = CRITICAL (fn () => Library.change database f);
 end;
 
 
@@ -150,7 +150,8 @@
     SOME thy => thy
   | NONE => error (loader_msg "nothing known about theory" [name]));
 
-fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
+fun change_thy name f = CRITICAL (fn () =>
+  (get_thy name; change_thys (Graph.map_node name f)));
 
 
 (* access deps *)
@@ -229,8 +230,9 @@
 
 fun outdate_thy name =
   if is_finished name orelse is_outdated name then ()
-  else (change_deps name (Option.map (fn {outdated = _, master, parents, files} =>
-    make_deps true master parents files)); perform Outdate name);
+  else CRITICAL (fn () =>
+   (change_deps name (Option.map (fn {outdated = _, master, parents, files} =>
+    make_deps true master parents files)); perform Outdate name));
 
 fun check_unfinished name =
   if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
@@ -317,9 +319,10 @@
     if null missing_files then ()
     else warning (loader_msg "unresolved dependencies of theory" [name] ^
       " on file(s): " ^ commas_quote missing_files);
-    change_deps name
-      (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files));
-    perform Update name
+    CRITICAL (fn () =>
+     (change_deps name
+        (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files));
+      perform Update name))
   end;
 
 
@@ -420,8 +423,7 @@
   else
     let val succs = thy_graph Graph.all_succs [name] in
       priority (loader_msg "removing" succs);
-      List.app (perform Remove) succs;
-      change_thys (Graph.del_nodes succs)
+      CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
     end;
 
 
@@ -496,7 +498,7 @@
   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; perform Update name)
+    else CRITICAL (fn () => (change_thys register; perform Update name))
   end;
 
 val _ = register_theory ProtoPure.thy;