src/Tools/Code/code_runtime.ML
changeset 45268 a42624e9de09
parent 44663 3bc39cfe27fe
child 45430 b8eb7a791dac
equal deleted inserted replaced
45267:66823a0066db 45268:a42624e9de09
   420   let
   420   let
   421     val thy' = Loaded_Values.put [] thy;
   421     val thy' = Loaded_Values.put [] thy;
   422     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   422     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   423     val _ = Secure.use_text notifying_context
   423     val _ = Secure.use_text notifying_context
   424       (0, Path.implode filepath) false (File.read filepath);
   424       (0, Path.implode filepath) false (File.read filepath);
   425     val thy'' = (Context.the_theory o the) (Context.thread_data ());
   425     val thy'' = Context.the_theory (Context.the_thread_data ());
   426     val names = Loaded_Values.get thy'';
   426     val names = Loaded_Values.get thy'';
   427   in (names, thy'') end;
   427   in (names, thy'') end;
   428 
   428 
   429 end;
   429 end;
   430 
   430