--- a/src/Pure/Thy/ml_context.ML Fri Apr 13 21:26:35 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML Fri Apr 13 21:38:29 2007 +0200
@@ -31,6 +31,7 @@
(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 * string) ref (* FIXME tmp *)
val use_mltext: string -> bool -> Context.generic option -> unit
val use_mltext_update: string -> bool -> Context.generic -> Context.generic
val use_let: string -> string -> string -> Context.generic -> Context.generic
@@ -164,9 +165,11 @@
in
+val eval_antiquotes_fn = ref eval_antiquotes;
+
fun eval_wrapper name verbose txt =
let
- val (txt1, txt2) = eval_antiquotes txt;
+ val (txt1, txt2) = ! eval_antiquotes_fn txt;
val _ =
if txt1 = isabelle_struct0 andalso txt2 = txt then ()
else Output.debug (fn () => cat_lines [txt1, txt2]);