# HG changeset patch
# User wenzelm
# Date 1208268738 -7200
# Node ID 5967c2a0a94f3e43a77db57134a57dc58f6021a9
# Parent  35249f5367b3145b5e5c974e2f54383cfb8dc48c
removed eval_antiquotes_fn;
eval: CRITICAL for now;

diff -r 35249f5367b3 -r 5967c2a0a94f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Apr 15 16:12:16 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 15 16:12:18 2008 +0200
@@ -30,7 +30,6 @@
     (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
   val proj_value_antiq: string -> (Context.generic * Args.T list ->
       (string * string * string) * (Context.generic * Args.T list)) -> unit
-  val eval_antiquotes_fn: (string -> string * Position.T -> string * string) ref  (* FIXME tmp *)
   val trace: bool ref
   val eval: bool -> Position.T -> string -> unit
   val eval_file: Path.T -> unit
@@ -165,8 +164,6 @@
 
 in
 
-val eval_antiquotes_fn = ref eval_antiquotes;
-
 val trace = ref false;
 
 fun eval_wrapper pr verbose pos txt =
@@ -174,13 +171,13 @@
     val struct_name =
       if Multithreading.available then "Isabelle" ^ serial_string ()
       else "Isabelle";
-    val (txt1, txt2) = ! eval_antiquotes_fn struct_name (txt, pos);  (* FIXME tmp hook *)
+    val (txt1, txt2) = eval_antiquotes struct_name (txt, pos);
     val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
     fun eval p =
       use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
   in
     eval Position.none false txt1;
-    eval pos verbose txt2;
+    NAMED_CRITICAL "ML" (fn () => eval pos verbose txt2); (* FIXME non-critical with local ML env *)
     forget_structure struct_name
   end;