# HG changeset patch
# User wenzelm
# Date 1199200169 -3600
# Node ID 9bc082c2cc92b3d9e99c51c291a8556b0a0cc87c
# Parent  842b85a79cb93c7017415edd97ba22de85f0dfe3
eval_wrapper: CRITICAL;
tuned;

diff -r 842b85a79cb9 -r 9bc082c2cc92 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Jan 01 16:09:28 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Jan 01 16:09:29 2008 +0100
@@ -175,7 +175,10 @@
     val (txt1, txt2) = ! eval_antiquotes_fn txt;  (* FIXME tmp hook *)
     val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
     fun eval nm = use_text nm pr;
-  in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
+  in
+    NAMED_CRITICAL "ML" (fn () =>
+      (eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0))
+  end;
 
 fun ML_wrapper pr = eval_wrapper "ML" pr;
 
@@ -188,7 +191,7 @@
   setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) ();
 
 fun use_mltext_update txt verbose context =
-  #2 (pass_context context (ML_wrapper Output.ml_output verbose) txt);
+  #2 (pass_context context (fn () => ML_wrapper Output.ml_output verbose txt) ());
 
 fun use_context txt = use_mltext_update
   ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;