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; |