src/Tools/Code/code_runtime.ML
changeset 62493 dd154240a53c
parent 62354 fdd6989cc8a0
child 62494 b90109b2487c
equal deleted inserted replaced
62492:0e53fade87fe 62493:dd154240a53c
    80 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    80 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    81 
    81 
    82 fun exec ctxt verbose code =
    82 fun exec ctxt verbose code =
    83  (if Config.get ctxt trace then tracing code else ();
    83  (if Config.get ctxt trace then tracing code else ();
    84   ML_Context.exec (fn () =>
    84   ML_Context.exec (fn () =>
    85     Secure.use_text ML_Env.local_context
    85     use_text ML_Env.local_context
    86       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    86       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    87 
    87 
    88 fun value ctxt (get, put, put_ml) (prelude, value) =
    88 fun value ctxt (get, put, put_ml) (prelude, value) =
    89   let
    89   let
    90     val code = (prelude
    90     val code = (prelude
   527     allType      = #allType ML_Env.local_name_space,
   527     allType      = #allType ML_Env.local_name_space,
   528     allFix       = #allFix ML_Env.local_name_space,
   528     allFix       = #allFix ML_Env.local_name_space,
   529     allStruct    = #allStruct ML_Env.local_name_space,
   529     allStruct    = #allStruct ML_Env.local_name_space,
   530     allSig       = #allSig ML_Env.local_name_space,
   530     allSig       = #allSig ML_Env.local_name_space,
   531     allFunct     = #allFunct ML_Env.local_name_space},
   531     allFunct     = #allFunct ML_Env.local_name_space},
   532   str_of_pos = #str_of_pos ML_Env.local_context,
   532   here = #here ML_Env.local_context,
   533   print = #print ML_Env.local_context,
   533   print = #print ML_Env.local_context,
   534   error = #error ML_Env.local_context};
   534   error = #error ML_Env.local_context};
   535 
   535 
   536 in
   536 in
   537 
   537 
   538 fun use_file filepath thy =
   538 fun use_file filepath thy =
   539   let
   539   let
   540     val thy' = Loaded_Values.put [] thy;
   540     val thy' = Loaded_Values.put [] thy;
   541     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   541     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   542     val _ =
   542     val _ =
   543       Secure.use_text notifying_context
   543       use_text notifying_context
   544         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   544         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   545         (File.read filepath);
   545         (File.read filepath);
   546     val thy'' = Context.the_theory (Context.the_thread_data ());
   546     val thy'' = Context.the_theory (Context.the_thread_data ());
   547     val names = Loaded_Values.get thy'';
   547     val names = Loaded_Values.get thy'';
   548   in (names, thy'') end;
   548   in (names, thy'') end;