clarified ML_environment: ML_write_global requires "Isabelle";
authorwenzelm
Tue Aug 28 11:13:33 2018 +0200 (13 months ago)
changeset 68826deefe5837120
parent 68825 8207c67d9ef4
child 68827 1286ca9dfd26
clarified ML_environment: ML_write_global requires "Isabelle";
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Pure.thy	Tue Aug 28 10:58:43 2018 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Aug 28 11:13:33 2018 +0200
     1.3 @@ -196,11 +196,14 @@
     1.4      (Parse.ML_source >> (fn source =>
     1.5        Toplevel.generic_theory (fn context =>
     1.6          context
     1.7 +        |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle
     1.8          |> Config.put_generic ML_Env.ML_write_global true
     1.9          |> ML_Context.exec (fn () =>
    1.10              ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
    1.11          |> Config.put_generic ML_Env.ML_write_global
    1.12              (Config.get_generic context ML_Env.ML_write_global)
    1.13 +        |> Config.put_generic ML_Env.ML_environment
    1.14 +            (Config.get_generic context ML_Env.ML_environment)
    1.15          |> Local_Theory.propagate_ml_env)));
    1.16  
    1.17  val _ =