# HG changeset patch
# User wenzelm
# Date 1199200168 -3600
# Node ID 842b85a79cb93c7017415edd97ba22de85f0dfe3
# Parent  99c9fc5e11f26dc3862ca13686d73271257f53bf
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;

diff -r 99c9fc5e11f2 -r 842b85a79cb9 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jan 01 16:09:27 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jan 01 16:09:28 2008 +0100
@@ -284,7 +284,9 @@
     else
       let
         val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
-        val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
+        val tr = Toplevel.imperative (fn () =>
+          ML_Context.setmp (SOME (Context.Theory (ThyInfo.get_theory name)))
+            (fn () => ThyInfo.load_file time path) ());
         val tr_name = if time then "time_use" else "use";
       in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
   end;
@@ -313,7 +315,6 @@
 
 fun load_thy dir name pos text time =
  (run_thy dir name pos text time;
-  CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))));
   try_ml_file dir name time);
 
 in