src/Tools/Code/code_runtime.ML
changeset 62902 3c0f53eae166
parent 62889 99c7f31615c2
child 63064 2f18172214c8
equal deleted inserted replaced
62901:0951d6cec68c 62902:3c0f53eae166
    79 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    79 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    80 
    80 
    81 fun exec ctxt verbose code =
    81 fun exec ctxt verbose code =
    82  (if Config.get ctxt trace then tracing code else ();
    82  (if Config.get ctxt trace then tracing code else ();
    83   ML_Context.exec (fn () =>
    83   ML_Context.exec (fn () =>
    84     ML_Compiler0.use_text ML_Env.context
    84     ML_Compiler0.ML ML_Env.context
    85       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    85       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    86 
    86 
    87 fun value ctxt (get, put, put_ml) (prelude, value) =
    87 fun value ctxt (get, put, put_ml) (prelude, value) =
    88   let
    88   let
    89     val code =
    89     val code =
   534 fun use_file filepath thy =
   534 fun use_file filepath thy =
   535   let
   535   let
   536     val thy' = Loaded_Values.put [] thy;
   536     val thy' = Loaded_Values.put [] thy;
   537     val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
   537     val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
   538     val _ =
   538     val _ =
   539       ML_Compiler0.use_text notifying_context
   539       ML_Compiler0.ML notifying_context
   540         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   540         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   541         (File.read filepath);
   541         (File.read filepath);
   542     val thy'' = Context.the_global_context ();
   542     val thy'' = Context.the_global_context ();
   543     val names = Loaded_Values.get thy'';
   543     val names = Loaded_Values.get thy'';
   544   in (names, thy'') end;
   544   in (names, thy'') end;