# HG changeset patch
# User wenzelm
# Date 1292956536 -3600
# Node ID 7a89b4b94817a7692da6c50caf7aacd0b17cb98f
# Parent  a35af5180c0104ff62507e68735a2b5a929f147b
configuration option "ML_trace";

diff -r a35af5180c01 -r 7a89b4b94817 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Dec 21 17:52:35 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Dec 21 19:35:36 2010 +0100
@@ -405,6 +405,7 @@
   register_config Syntax.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
   register_config Syntax.eta_contract_raw #>
+  register_config ML_Context.trace_raw #>
   register_config ProofContext.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
   register_config Goal_Display.show_main_goal_raw #>
diff -r a35af5180c01 -r 7a89b4b94817 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Dec 21 17:52:35 2010 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Dec 21 19:35:36 2010 +0100
@@ -25,7 +25,8 @@
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
-  val trace: bool Unsynchronized.ref
+  val trace_raw: Config.raw
+  val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -172,7 +173,8 @@
         in (ml, SOME (Context.Proof ctxt')) end;
   in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val trace = Unsynchronized.ref false;
+val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
+val trace = Config.bool trace_raw;
 
 fun eval verbose pos ants =
   let
@@ -181,8 +183,12 @@
       eval_antiquotes (ants, pos) (Context.thread_data ())
       ||> Option.map (Context.mapping I (Context_Position.set_visible false));
     val _ =
-      if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
-      else ();
+      (case env_ctxt of
+        SOME context =>
+          if Config.get (Context.proof_of context) trace then
+            tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+          else ()
+      | NONE => ());
 
     (*prepare static ML environment*)
     val _ = Context.setmp_thread_data env_ctxt