# HG changeset patch
# User wenzelm
# Date 1186173187 -7200
# Node ID 1b2f1a1a03a341961e7b4e0303d21563e645cfc7
# Parent  2d4ee876c215d7ee9f482a8064fd349293a1d839
use separate trace flag instead of Output.debug;

diff -r 2d4ee876c215 -r 1b2f1a1a03a3 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Fri Aug 03 22:33:03 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Fri Aug 03 22:33:07 2007 +0200
@@ -32,6 +32,7 @@
   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 trace: bool ref
   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
@@ -167,12 +168,12 @@
 
 val eval_antiquotes_fn = ref eval_antiquotes;
 
+val trace = ref false;
+
 fun eval_wrapper name verbose txt =
   let
     val (txt1, txt2) = ! eval_antiquotes_fn txt;
-    val _ =
-      if txt1 = isabelle_struct0 andalso txt2 = txt then ()
-      else Output.debug (fn () => cat_lines [txt1, txt2]);
+    val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
   in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
 
 end;