# HG changeset patch
# User wenzelm
# Date 1288085007 -7200
# Node ID 752a26dce4bea78413c51cd350f24521e72f4827
# Parent  1348d4982a1776802a91cbbda670941e6f804390# Parent  4c35be108990cd375a0a27b2b53d915766a36fff
merged

diff -r 4c35be108990 -r 752a26dce4be src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Oct 26 11:22:18 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Oct 26 11:23:27 2010 +0200
@@ -29,6 +29,7 @@
     -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
+  val trace: bool Unsynchronized.ref
   val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
 end;
 
@@ -59,8 +60,11 @@
   #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
        (*avoid further pervasive infix names*)
 
+val trace = Unsynchronized.ref false;
+
 fun exec verbose code =
-  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code);
+  (if ! trace then tracing code else ();
+  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let