Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorblanchet
Tue, 26 Oct 2010 11:21:08 +0200
changeset 40159 bfc716a96e47
parent 40158 a88d6073b190 (current diff)
parent 40150 1348d4982a17 (diff)
child 40160 539351451286
merge
--- 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
isabelle