# HG changeset patch
# User wenzelm
# Date 1185786748 -7200
# Node ID 82873bc360c220868fec0e344c8c54072c934db1
# Parent  ff4c715a11cd2f0e9d7ecff5f95a3eb05434ba0b
marked some CRITICAL sections;

diff -r ff4c715a11cd -r 82873bc360c2 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Jul 30 10:39:12 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 30 11:12:28 2007 +0200
@@ -315,7 +315,8 @@
 val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
-  (ML_Context.set_context (try Toplevel.generic_theory_of state); raise Toplevel.TERMINATE));
+ (CRITICAL (fn () => ML_Context.set_context (try Toplevel.generic_theory_of state));
+  raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;
 
diff -r ff4c715a11cd -r 82873bc360c2 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 30 10:39:12 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 30 11:12:28 2007 +0200
@@ -280,7 +280,7 @@
 
 fun load_thy dir name pos text ml time =
  (run_thy dir name pos text time;
-  ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
+  CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))));
   if ml then try_ml_file dir name time else ());
 
 in
@@ -296,7 +296,7 @@
 (* main loop *)
 
 fun gen_loop term =
- (ML_Context.set_context NONE;
+ (CRITICAL (fn () => ML_Context.set_context NONE);
   Toplevel.loop (isar term));
 
 fun gen_main term =
diff -r ff4c715a11cd -r 82873bc360c2 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jul 30 10:39:12 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 30 11:12:28 2007 +0200
@@ -454,7 +454,7 @@
   let val name = base_name str in
     check_unfinished warning name;
     gen_use_thy' req Path.current str;
-    ML_Context.set_context (SOME (Context.Theory (get_theory name)))
+    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name))))
   end;
 
 in
@@ -497,7 +497,8 @@
     val _ = check_unfinished error name;
     val _ = if int then quiet_update_thys dir parents else ();
     (* FIXME tmp *)
-    val _ = ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names))));
+    val _ = CRITICAL (fn () =>
+      ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))));
     val _ = check_uses name uses;
 
     val theory =