# HG changeset patch # User haftmann # Date 1291885113 -3600 # Node ID 5cf62cefbbb4d9a9716b1825bbbee1ee2ae924f8 # Parent 1dc7652ce404e538f084499b3f6844729b41f113 tracing of term to be evaluated diff -r 1dc7652ce404 -r 5cf62cefbbb4 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;