tracing of term to be evaluated
authorhaftmann
Thu, 09 Dec 2010 09:58:33 +0100
changeset 41099 5cf62cefbbb4
parent 41094 1dc7652ce404
child 41100 6c0940392fb4
tracing of term to be evaluated
src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Dec 09 08:46:04 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Dec 09 09:58:33 2010 +0100
@@ -115,6 +115,9 @@
 fun dynamic_value_exn cookie thy some_target postproc t args =
   let
     val _ = reject_vars thy t;
+    val _ = if ! trace
+      then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
+      else ()
     fun evaluator naming program ((_, vs_ty), t) deps =
       base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
   in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;