support named ML environments, notably "Isabelle", "SML";
more uniform options ML_read_global, ML_write_global;
clarified bootstrap environment;

--- a/src/FOL/IFOL.thy	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/FOL/IFOL.thy	Mon Aug 27 14:42:24 2018 +0200
@@ -8,6 +8,7 @@
 imports Pure
 begin
 
+ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
 ML_file "~~/src/Tools/misc_legacy.ML"
 ML_file "~~/src/Provers/splitter.ML"
 ML_file "~~/src/Provers/hypsubst.ML"

--- a/src/Pure/Isar/attrib.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -587,6 +587,9 @@
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
   register_config ML_Print_Depth.print_depth_raw #>
+  register_config ML_Env.ML_environment_raw #>
+  register_config ML_Env.ML_read_global_raw #>
+  register_config ML_Env.ML_write_global_raw #>
   register_config ML_Options.source_trace_raw #>
   register_config ML_Options.exception_trace_raw #>
   register_config ML_Options.exception_debugger_raw #>

--- a/src/Pure/ML/ml_compiler.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+    {read: string option, write: string option, redirect: bool, verbose: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
@@ -21,17 +21,17 @@
 (* flags *)
 
 type flags =
-  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+  {read: string option, write: string option, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {SML = false, exchange = false, redirect = false, verbose = false,
+  {read = NONE, write = NONE, redirect = false, verbose = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
+  {read = #read flags, write = #write flags, redirect = #redirect flags, verbose = b,
     debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
 
@@ -154,14 +154,14 @@
     val opt_context = Context.get_generic_context ();
 
     val env as {debug, name_space, add_breakpoints} =
-      (case (ML_Recursive.get (), #SML flags orelse #exchange flags) of
+      (case (ML_Recursive.get (), is_some (#read flags) orelse is_some (#write flags)) of
         (SOME env, false) => env
       | _ =>
        {debug =
           (case #debug flags of
             SOME debug => debug
           | NONE => ML_Options.debugger_enabled opt_context),
-        name_space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags},
+        name_space = ML_Env.make_name_space {read = #read flags, write = #write flags},
         add_breakpoints = ML_Env.add_breakpoints});
 
 
@@ -170,7 +170,7 @@
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_explode =
-      if #SML flags then String.explode
+      if ML_Env.is_standard (ML_Env.default_env (#read flags)) then String.explode
       else maps (String.explode o Symbol.esc) o Symbol.explode;
 
     fun token_content tok =

--- a/src/Pure/ML/ml_context.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -195,7 +195,8 @@
   in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
-  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
+  eval flags (Input.pos_of source)
+    (ML_Lex.read_source (ML_Env.is_standard (ML_Env.default_env (#read flags))) source);
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_generic_context (Option.map Context.Proof ctxt)

--- a/src/Pure/ML/ml_env.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -7,16 +7,26 @@
 
 signature ML_ENV =
 sig
+  val Isabelle: string
+  val SML: string
+  val is_standard: string -> bool
+  val make_standard: bool -> string
+  val ML_environment_raw: Config.raw
+  val ML_environment: string Config.T
+  val ML_read_global_raw: Config.raw
+  val ML_read_global: bool Config.T
+  val ML_write_global_raw: Config.raw
+  val ML_write_global: bool Config.T
+  val context_env: Context.generic -> string option -> string
+  val default_env: string option -> string
   val inherit: Context.generic -> Context.generic -> Context.generic
-  val forget_structure: string -> Context.generic -> Context.generic
+  val setup: string -> theory -> theory
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
   val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
-  val init_bootstrap: Context.generic -> Context.generic
-  val SML_environment: bool Config.T
-  val set_global: bool -> Context.generic -> Context.generic
-  val restore_global: Context.generic -> Context.generic -> Context.generic
-  val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
-  val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
+  val forget_structure: string -> Context.generic -> Context.generic
+  val bootstrap_name_space: Context.generic -> Context.generic
+  val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
+  val make_name_space: {read: string option, write: string option} -> ML_Name_Space.T
   val context: ML_Compiler0.context
   val name_space: ML_Name_Space.T
   val check_functor: string -> unit
@@ -25,6 +35,39 @@
 structure ML_Env: ML_ENV =
 struct
 
+(* named environments *)
+
+val Isabelle = "Isabelle";
+val SML = "SML";
+
+fun is_standard env = env <> Isabelle;
+fun make_standard sml = if sml then SML else Isabelle;
+
+val ML_environment_raw = Config.declare ("ML_environment", \<^here>) (fn _ => Config.String Isabelle);
+val ML_environment = Config.string ML_environment_raw;
+
+fun context_env _ (SOME name) = name
+  | context_env context NONE = Config.get_generic context ML_environment;
+
+fun default_env (SOME name) = name
+  | default_env NONE =
+      (case Context.get_generic_context () of
+        NONE => Isabelle
+      | SOME context => context_env context NONE);
+
+
+(* global read/write *)
+
+val ML_read_global_raw = Config.declare ("ML_read_global", \<^here>) (fn _ => Config.Bool true);
+val ML_write_global_raw = Config.declare ("ML_write_global", \<^here>) (fn _ => Config.Bool true);
+
+val ML_read_global = Config.bool ML_read_global_raw;
+val ML_write_global = Config.bool ML_write_global_raw;
+
+fun read_global context = Config.get_generic context ML_read_global;
+fun write_global context = Config.get_generic context ML_write_global;
+
+
 (* name space tables *)
 
 type tables =
@@ -56,141 +99,120 @@
    Symtab.make ML_Name_Space.sml_signature,
    Symtab.make ML_Name_Space.sml_functor);
 
-fun bootstrap_tables ((val1, type1, fixity1, structure1, signature1, functor1): tables) : tables =
-  let
-    val val2 =
-      fold (fn (x, y) =>
-        member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
-      (#allVal ML_Name_Space.global ()) val1;
-    val structure2 =
-      fold (fn (x, y) =>
-        member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
-      (#allStruct ML_Name_Space.global ()) structure1;
-    val signature2 =
-      fold (fn (x, y) =>
-        member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
-      (#allSig ML_Name_Space.global ()) signature1;
-  in (val2, type1, fixity1, structure2, signature2, functor1) end;
-
 
 (* context data *)
 
 type data =
- {global: bool,
-  tables: tables,
-  sml_tables: tables,
+ {envs: tables Name_Space.table,
   breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
 
-fun make_data (global, tables, sml_tables, breakpoints) : data =
-  {global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
+fun make_data (envs, breakpoints) : data = {envs = envs, breakpoints = breakpoints};
 
-structure Env = Generic_Data
+structure Data = Generic_Data
 (
   type T = data
-  val empty = make_data (true, empty_tables, sml_tables, Inttab.empty);
-  fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
+  val empty = make_data (Name_Space.empty_table "ML_environment", Inttab.empty);
+  fun extend (data : T) = make_data (#envs data, #breakpoints data);
   fun merge (data : T * T) =
-    make_data (false,
-      merge_tables (apply2 #tables data),
-      merge_tables (apply2 #sml_tables data),
+    make_data ((apply2 #envs data) |> Name_Space.join_tables (K merge_tables),
       Inttab.merge (K true) (apply2 #breakpoints data));
 );
 
-val inherit = Env.put o Env.get;
+val inherit = Data.put o Data.get;
 
-fun forget_structure name =
-  Env.map (fn {global, tables, sml_tables, breakpoints} =>
+fun setup env_name thy =
+  thy |> (Context.theory_map o Data.map) (fn {envs, breakpoints} =>
     let
-      val _ = if global then ML_Name_Space.forget_structure name else ();
-      val tables' =
-        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
-    in make_data (global, tables', sml_tables, breakpoints) end);
-
-val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
+      val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
+      val tables = if env_name = Isabelle then empty_tables else sml_tables;
+      val (_, envs') = envs
+        |> Name_Space.define (Context.Theory thy') true (Binding.name env_name, tables);
+    in make_data (envs', breakpoints) end);
 
-fun add_breakpoints more_breakpoints =
-  if is_some (Context.get_generic_context ()) then
-    Context.>>
-      (Env.map (fn {global, tables, sml_tables, breakpoints} =>
-        let val breakpoints' =
-          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
-        in make_data (global, tables, sml_tables, breakpoints') end))
-  else ();
-
+val get_env = Name_Space.get o #envs o Data.get;
 
-(* SML environment for Isabelle/ML *)
-
-val SML_environment =
-  Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
+fun update_env env_name f context = context |> Data.map (fn {envs, breakpoints} =>
+  let
+    val _ = Name_Space.get envs env_name;
+    val envs' = Name_Space.map_table_entry env_name f envs;
+  in make_data (envs', breakpoints) end);
 
-fun sml_env SML =
-  SML orelse
-    (case Context.get_generic_context () of
-      NONE => false
-    | SOME context => Config.get_generic context SML_environment);
+fun forget_structure name context =
+  (if write_global context then ML_Name_Space.forget_structure name else ();
+    context |> update_env Isabelle (fn tables =>
+      (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables)));
 
 
 (* name space *)
 
-val init_bootstrap =
-  Env.map (fn {global, tables, sml_tables, breakpoints} =>
-    make_data (global, tables, bootstrap_tables sml_tables, breakpoints));
+val bootstrap_name_space =
+  update_env Isabelle (fn (tables: tables) =>
+    let
+      fun update entries (x, y) = member (op =) entries x ? Symtab.update (x, y);
+      val bootstrap_val = update ML_Name_Space.bootstrap_values;
+      val bootstrap_structure = update ML_Name_Space.bootstrap_structures;
+      val bootstrap_signature = update ML_Name_Space.bootstrap_signatures;
 
-fun set_global global =
-  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
-    make_data (global, tables, sml_tables, breakpoints));
+      val (val1, type1, fixity1, structure1, signature1, functor1) = sml_tables;
+      val val2 = val1
+        |> fold bootstrap_val (#allVal ML_Name_Space.global ())
+        |> Symtab.fold bootstrap_val (#1 tables);
+      val structure2 = structure1
+        |> fold bootstrap_structure (#allStruct ML_Name_Space.global ())
+        |> Symtab.fold bootstrap_structure (#4 tables);
+      val signature2 = signature1
+        |> fold bootstrap_signature (#allSig ML_Name_Space.global ())
+        |> Symtab.fold bootstrap_signature (#5 tables);
+    in (val2, type1, fixity1, structure2, signature2, functor1) end);
 
-val restore_global = set_global o #global o Env.get;
-
-fun add_name_space {SML} (space: ML_Name_Space.T) =
-  Env.map (fn {global, tables, sml_tables, breakpoints} =>
+fun add_name_space env (space: ML_Name_Space.T) =
+  update_env env (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
     let
-      val (tables', sml_tables') =
-        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
-          (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
-            let
-              val val2 = fold Symtab.update (#allVal space ()) val1;
-              val type2 = fold Symtab.update (#allType space ()) type1;
-              val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
-              val structure2 = fold Symtab.update (#allStruct space ()) structure1;
-              val signature2 = fold Symtab.update (#allSig space ()) signature1;
-              val functor2 = fold Symtab.update (#allFunct space ()) functor1;
-            in (val2, type2, fixity2, structure2, signature2, functor2) end);
-    in make_data (global, tables', sml_tables', breakpoints) end);
+      val val2 = fold Symtab.update (#allVal space ()) val1;
+      val type2 = fold Symtab.update (#allType space ()) type1;
+      val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
+      val structure2 = fold Symtab.update (#allStruct space ()) structure1;
+      val signature2 = fold Symtab.update (#allSig space ()) signature1;
+      val functor2 = fold Symtab.update (#allFunct space ()) functor1;
+    in (val2, type2, fixity2, structure2, signature2, functor2) end);
+
+fun make_name_space {read, write} : ML_Name_Space.T =
+  let
+    val read_env = default_env read;
+    val write_env = default_env write;
 
-fun make_name_space {SML, exchange} : ML_Name_Space.T =
-  let
+    fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_env context read_env)) name;
+    fun dest_env sel1 context = Symtab.dest (sel1 (get_env context read_env));
+    fun enter_env ap1 entry = update_env write_env (ap1 (Symtab.update entry));
+
     fun lookup sel1 sel2 name =
-      if sml_env SML then
-        Context.the_generic_context ()
-        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
-      else
-        Context.get_generic_context ()
-        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
-        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+      if read_env = Isabelle then
+        (case Context.get_generic_context () of
+          NONE => sel2 ML_Name_Space.global name
+        | SOME context =>
+            (case lookup_env sel1 context name of
+              NONE => if read_global context then sel2 ML_Name_Space.global name else NONE
+            | some => some))
+      else lookup_env sel1 (Context.the_generic_context ()) name;
 
     fun all sel1 sel2 () =
-      (if sml_env SML then
-        Context.the_generic_context ()
-        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
-      else
-        Context.get_generic_context ()
-        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
-        |> append (sel2 ML_Name_Space.global ()))
-      |> sort_distinct (string_ord o apply2 #1);
+      sort_distinct (string_ord o apply2 #1)
+        (if read_env = Isabelle then
+          (case Context.get_generic_context () of
+            NONE => sel2 ML_Name_Space.global ()
+          | SOME context =>
+              dest_env sel1 context @
+              (if read_global context then sel2 ML_Name_Space.global () else []))
+         else dest_env sel1 (Context.the_generic_context ()));
 
     fun enter ap1 sel2 entry =
-      if sml_env SML <> exchange then
-        Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} =>
-          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
-          in make_data (global, tables, sml_tables', breakpoints) end))
-      else if is_some (Context.get_generic_context ()) then
-        Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} =>
-          let
-            val _ = if global then sel2 ML_Name_Space.global entry else ();
-            val tables' = ap1 (Symtab.update entry) tables;
-          in make_data (global, tables', sml_tables, breakpoints) end))
-      else sel2 ML_Name_Space.global entry;
+      if write_env = Isabelle then
+        (case Context.get_generic_context () of
+          NONE => sel2 ML_Name_Space.global entry
+        | SOME context =>
+            (if write_global context then sel2 ML_Name_Space.global entry else ();
+             Context.>> (enter_env ap1 entry)))
+      else Context.>> (enter_env ap1 entry);
   in
    {lookupVal    = lookup #1 #lookupVal,
     lookupType   = lookup #2 #lookupType,
@@ -213,7 +235,7 @@
   end;
 
 val context: ML_Compiler0.context =
- {name_space = make_name_space {SML = false, exchange = false},
+ {name_space = make_name_space {read = NONE, write = NONE},
   print_depth = NONE,
   here = Position.here oo Position.line_file,
   print = writeln,
@@ -227,4 +249,20 @@
   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   else error ("Unknown ML functor: " ^ quote name);
 
+
+(* breakpoints *)
+
+val get_breakpoint = Inttab.lookup o #breakpoints o Data.get;
+
+fun add_breakpoints more_breakpoints =
+  if is_some (Context.get_generic_context ()) then
+    Context.>>
+      (Data.map (fn {envs, breakpoints} =>
+        let val breakpoints' =
+          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
+        in make_data (envs, breakpoints') end))
+  else ();
+
 end;
+
+Theory.setup (ML_Env.setup ML_Env.Isabelle #> ML_Env.setup ML_Env.SML);

--- a/src/Pure/ML/ml_file.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/ML/ml_file.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -6,6 +6,8 @@
 
 signature ML_FILE =
 sig
+  val command: string option -> bool option -> (theory -> Token.file list) ->
+    Toplevel.transition -> Toplevel.transition
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
@@ -13,7 +15,7 @@
 structure ML_File: ML_FILE =
 struct
 
-fun command SML debug files = Toplevel.generic_theory (fn gthy =>
+fun command env debug files = Toplevel.generic_theory (fn gthy =>
   let
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
@@ -21,8 +23,8 @@
 
     val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
-    val flags =
-      {SML = SML, exchange = false, redirect = true, verbose = true,
+    val flags: ML_Compiler.flags =
+      {read = env, write = env, redirect = true, verbose = true,
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
@@ -31,7 +33,7 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command false;
-val SML = command true;
+val ML = command NONE;
+val SML = command (SOME ML_Env.SML);
 
 end;

--- a/src/Pure/ML_Bootstrap.thy	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Mon Aug 27 14:42:24 2018 +0200
@@ -11,35 +11,37 @@
 external_file "$POLYML_EXE"
 
 
-subsection \<open>Standard ML environment for virtual bootstrap\<close>
+subsection \<open>ML environment for virtual bootstrap\<close>
 
-setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
-
-SML_import \<open>
+ML \<open>
+  #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
+    if member (op =) ML_Name_Space.hidden_structures name then
+      ML (Input.string ("structure " ^ name ^ " = " ^ name))
+    else ());
   structure Output_Primitives = Output_Primitives_Virtual;
   structure Thread_Data = Thread_Data_Virtual;
+  structure PolyML = PolyML;
   fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
 \<close>
 
 
-subsection \<open>Final setup of global ML environment\<close>
+subsection \<open>Global ML environment for Isabelle/Pure\<close>
 
 ML \<open>Proofterm.proofs := 0\<close>
 
-ML_export \<open>
-  List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
-  structure PolyML =
-  struct
-    val pointerEq = pointer_eq;
-    structure IntInf = PolyML.IntInf;
-  end;
+ML \<open>
+  Context.setmp_generic_context NONE
+    ML \<open>
+      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
+      structure PolyML =
+      struct
+        val pointerEq = pointer_eq;
+        structure IntInf = PolyML.IntInf;
+      end;
+    \<close>
 \<close>
 
-ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
-
-
-subsection \<open>Switch to bootstrap environment\<close>
-
-setup \<open>Config.put_global ML_Env.SML_environment true\<close>
+setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
+declare [[ML_read_global = false]]
 
 end

--- a/src/Pure/Pure.thy	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/Pure.thy	Mon Aug 27 14:42:24 2018 +0200
@@ -170,7 +170,7 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
+          {read = SOME ML_Env.SML, write = NONE, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
@@ -182,7 +182,7 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
+          {read = NONE, write = SOME ML_Env.SML, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
@@ -196,10 +196,11 @@
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory (fn context =>
         context
-        |> ML_Env.set_global true
+        |> Config.put_generic ML_Env.ML_write_global true
         |> ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
-        |> ML_Env.restore_global context
+        |> Config.put_generic ML_Env.ML_write_global
+            (Config.get_generic context ML_Env.ML_write_global)
         |> Local_Theory.propagate_ml_env)));
 
 val _ =
@@ -1440,4 +1441,6 @@
   qed
 qed
 
+declare [[ML_write_global = false]]
+
 end

--- a/src/Pure/Tools/debugger.ML	Mon Aug 27 14:31:52 2018 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 14:42:24 2018 +0200
@@ -132,15 +132,17 @@
     "Context.put_generic_context (SOME ML_context)"];
 
 fun evaluate {SML, verbose} =
-  ML_Context.eval
-    {SML = SML, exchange = false, redirect = false, verbose = verbose,
-      debug = SOME false, writeln = writeln_message, warning = warning_message}
-    Position.none;
+  let val env = ML_Env.make_standard SML in
+    ML_Context.eval
+      {read = SOME env, write = SOME env, redirect = false, verbose = verbose,
+        debug = SOME false, writeln = writeln_message, warning = warning_message}
+      Position.none
+  end;
 
 fun eval_setup thread_name index SML context =
   context
   |> Context_Position.set_visible_generic false
-  |> ML_Env.add_name_space {SML = SML}
+  |> ML_Env.add_name_space (ML_Env.make_standard SML)
       (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
 
 fun eval_context thread_name index SML toks =