# HG changeset patch
# User wenzelm
# Date 1280929549 -7200
# Node ID 675827e61eb9f40406f4746762b350fa6258d7bc
# Parent  d590ee2c191e3a108d57885cdb4a85294d736b88
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;

diff -r d590ee2c191e -r 675827e61eb9 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:14:48 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:45:49 2010 +0200
@@ -34,7 +34,7 @@
 local
   val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
+  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);
 end;
 
@@ -75,7 +75,7 @@
   val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
 in
   fun get_thys () = ! database;
-  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
+  fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
 end;
 
 
@@ -124,10 +124,10 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
-fun loaded_files name =
+fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   (case get_deps name of
     NONE => []
-  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
+  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
 
 
 
@@ -135,7 +135,7 @@
 
 (* remove theory *)
 
-fun remove_thy name = CRITICAL (fn () =>
+fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if is_finished name then error (loader_msg "attempt to change finished theory" [name])
   else
     let
@@ -145,7 +145,7 @@
       val _ = change_thys (Graph.del_nodes succs);
     in () end);
 
-fun kill_thy name = CRITICAL (fn () =>
+fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if known_thy name then remove_thy name
   else ());
 
@@ -236,7 +236,7 @@
     val parent_names = map Context.theory_name parent_thys;
     fun after_load' () =
      (after_load ();
-      CRITICAL (fn () =>
+      NAMED_CRITICAL "Thy_Info" (fn () =>
         (change_thys (new_entry name parent_names (SOME deps, SOME theory));
           perform Update name)));
 
@@ -333,7 +333,7 @@
     val parents = map Context.theory_name (Theory.parents_of theory);
     val deps = make_deps master parents;
   in
-    CRITICAL (fn () =>
+    NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
       priority ("Registering theory " ^ quote name);
       map get_theory parents;