# HG changeset patch
# User blanchet
# Date 1288084868 -7200
# Node ID bfc716a96e47284b51cda813a12450b797a608f7
# Parent  a88d6073b190197f4737f8a0d7cb8f51e2756a23# Parent  1348d4982a1776802a91cbbda670941e6f804390
merge

diff -r a88d6073b190 -r bfc716a96e47 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Oct 26 11:11:23 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Oct 26 11:21:08 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