src/Tools/Code/code_runtime.ML
changeset 63163 b561284a4214
parent 63160 80a91e0e236e
child 63164 72aaf69328fc
     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 @@ -78,11 +78,11 @@
     1.4  
     1.5  val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
     1.6  
     1.7 -fun exec ctxt verbose code =
     1.8 - (if Config.get ctxt trace then tracing code else ();
     1.9 -  ML_Context.exec (fn () =>
    1.10 -    ML_Compiler0.ML ML_Env.context
    1.11 -      {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    1.12 +fun compile_ML verbose code context =
    1.13 + (if Config.get_generic context trace then tracing code else ();
    1.14 +  ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
    1.15 +    {line = 0, file = "generated code", verbose = verbose,
    1.16 +       debug = false} code) context);
    1.17  
    1.18  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.19    let
    1.20 @@ -91,7 +91,7 @@
    1.21        put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    1.22      val ctxt' = ctxt
    1.23        |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    1.24 -      |> Context.proof_map (exec ctxt false code);
    1.25 +      |> Context.proof_map (compile_ML false code);
    1.26    in get ctxt' () end;
    1.27  
    1.28  
    1.29 @@ -416,7 +416,7 @@
    1.30  fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
    1.31        thy
    1.32        |> Code_Target.add_reserved target module_name
    1.33 -      |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code)
    1.34 +      |> Context.theory_map (compile_ML true code)
    1.35        |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
    1.36        |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
    1.37        |> fold (add_eval_const o apsnd Code_Printer.str) const_map