# HG changeset patch
# User wenzelm
# Date 1280867323 -7200
# Node ID c202426474c3985a40f90ceb4d14b6685b43fc7f
# Parent  8a2bacb8ad87c67cb189e7e9e69f90e032b2ed6b
more precise CRITICAL sections;
tuned;

diff -r 8a2bacb8ad87 -r c202426474c3 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 21:34:38 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 22:28:43 2010 +0200
@@ -116,7 +116,7 @@
 
 fun lookup_theory name =
   (case lookup_thy name of
-    SOME (_, SOME thy) => SOME thy
+    SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
 fun get_theory name =
@@ -135,19 +135,19 @@
 
 (* remove theory *)
 
-fun remove_thy name =
+fun remove_thy name = CRITICAL (fn () =>
   if is_finished name then error (loader_msg "attempt to change finished theory" [name])
   else
     let
       val succs = thy_graph Graph.all_succs [name];
       val _ = priority (loader_msg "removing" succs);
-      val _ = CRITICAL (fn () =>
-        (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
-    in () end;
+      val _ = List.app (perform Remove) succs;
+      val _ = change_thys (Graph.del_nodes succs);
+    in () end);
 
-fun kill_thy name =
+fun kill_thy name = CRITICAL (fn () =>
   if known_thy name then remove_thy name
-  else ();
+  else ());
 
 
 (* scheduling loader tasks *)
@@ -335,15 +335,14 @@
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val _ = kill_thy name;
-    val _ = priority ("Registering theory " ^ quote name);
-
     val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
     val deps = make_deps master parents;
   in
     CRITICAL (fn () =>
-     (map get_theory parents;
+     (kill_thy name;
+      priority ("Registering theory " ^ quote name);
+      map get_theory parents;
       change_thys (new_entry name parents (SOME deps, SOME theory));
       perform Update name))
   end;