equal
deleted
inserted
replaced
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; |