src/Tools/Code/code_runtime.ML
changeset 41099 5cf62cefbbb4
parent 40726 16dcfedc4eb7
child 41101 c1d1ec5b90f1
equal deleted inserted replaced
41094:1dc7652ce404 41099:5cf62cefbbb4
   113     | General.Fail _ => NONE;
   113     | General.Fail _ => NONE;
   114 
   114 
   115 fun dynamic_value_exn cookie thy some_target postproc t args =
   115 fun dynamic_value_exn cookie thy some_target postproc t args =
   116   let
   116   let
   117     val _ = reject_vars thy t;
   117     val _ = reject_vars thy t;
       
   118     val _ = if ! trace
       
   119       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
       
   120       else ()
   118     fun evaluator naming program ((_, vs_ty), t) deps =
   121     fun evaluator naming program ((_, vs_ty), t) deps =
   119       base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
   122       base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
   120   in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
   123   in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
   121 
   124 
   122 fun dynamic_value_strict cookie thy some_target postproc t args =
   125 fun dynamic_value_strict cookie thy some_target postproc t args =