src/Tools/Code/code_runtime.ML
changeset 60956 10d463883dc2
parent 59936 b8ffc3dc9e24
child 61077 06cca32aa519
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Aug 17 15:29:30 2015 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Aug 17 16:27:12 2015 +0200
     1.3 @@ -80,8 +80,10 @@
     1.4  val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
     1.5  
     1.6  fun exec ctxt verbose code =
     1.7 -  (if Config.get ctxt trace then tracing code else ();
     1.8 -  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
     1.9 + (if Config.get ctxt trace then tracing code else ();
    1.10 +  ML_Context.exec (fn () =>
    1.11 +    Secure.use_text ML_Env.local_context
    1.12 +      {line = 0, file = "generated code", verbose = verbose, debug = false} code));
    1.13  
    1.14  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.15    let
    1.16 @@ -538,8 +540,10 @@
    1.17    let
    1.18      val thy' = Loaded_Values.put [] thy;
    1.19      val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
    1.20 -    val _ = Secure.use_text notifying_context
    1.21 -      (0, Path.implode filepath) false (File.read filepath);
    1.22 +    val _ =
    1.23 +      Secure.use_text notifying_context
    1.24 +        {line = 0, file = Path.implode filepath, verbose = false, debug = false}
    1.25 +        (File.read filepath);
    1.26      val thy'' = Context.the_theory (Context.the_thread_data ());
    1.27      val names = Loaded_Values.get thy'';
    1.28    in (names, thy'') end;