src/Tools/Code/code_runtime.ML
changeset 63164 72aaf69328fc
parent 63163 b561284a4214
child 63174 57c0d60e491c
child 63178 b9e1d53124f5
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -80,9 +80,10 @@
     1.4  
     1.5  fun compile_ML verbose code context =
     1.6   (if Config.get_generic context trace then tracing code else ();
     1.7 -  ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
     1.8 +  Code_Preproc.timed "compiling ML" Context.proof_of
     1.9 +    (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
    1.10      {line = 0, file = "generated code", verbose = verbose,
    1.11 -       debug = false} code) context);
    1.12 +       debug = false} code)) context);
    1.13  
    1.14  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.15    let
    1.16 @@ -92,7 +93,8 @@
    1.17      val ctxt' = ctxt
    1.18        |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    1.19        |> Context.proof_map (compile_ML false code);
    1.20 -  in get ctxt' () end;
    1.21 +    val computator = get ctxt';
    1.22 +  in Code_Preproc.timed_exec "running ML" computator ctxt' end;
    1.23  
    1.24  
    1.25  (* computation as evaluation into ML language values *)
    1.26 @@ -300,7 +302,10 @@
    1.27      val ml_name_for_const = the o AList.lookup (op =) const_map;
    1.28      val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs
    1.29      val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
    1.30 -  in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end;
    1.31 +  in
    1.32 +    Code_Preproc.timed_value "computing" 
    1.33 +      (fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t)
    1.34 +  end;
    1.35  
    1.36  fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
    1.37    let