support named ML environments, notably "Isabelle", "SML";
authorwenzelm
Mon Aug 27 14:42:24 2018 +0200 (13 months ago)
changeset 688165a53724fe247
parent 68815 6296915dee6e
child 68817 b9568a82b474
support named ML environments, notably "Isabelle", "SML";
more uniform options ML_read_global, ML_write_global;
clarified bootstrap environment;
src/FOL/IFOL.thy
src/Pure/Isar/attrib.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_file.ML
src/Pure/ML_Bootstrap.thy
src/Pure/Pure.thy
src/Pure/Tools/debugger.ML
     1.1 --- a/src/FOL/IFOL.thy	Mon Aug 27 14:31:52 2018 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Mon Aug 27 14:42:24 2018 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  imports Pure
     1.5  begin
     1.6  
     1.7 +ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
     1.8  ML_file "~~/src/Tools/misc_legacy.ML"
     1.9  ML_file "~~/src/Provers/splitter.ML"
    1.10  ML_file "~~/src/Provers/hypsubst.ML"
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 27 14:31:52 2018 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 27 14:42:24 2018 +0200
     2.3 @@ -587,6 +587,9 @@
     2.4    register_config Name_Space.names_short_raw #>
     2.5    register_config Name_Space.names_unique_raw #>
     2.6    register_config ML_Print_Depth.print_depth_raw #>
     2.7 +  register_config ML_Env.ML_environment_raw #>
     2.8 +  register_config ML_Env.ML_read_global_raw #>
     2.9 +  register_config ML_Env.ML_write_global_raw #>
    2.10    register_config ML_Options.source_trace_raw #>
    2.11    register_config ML_Options.exception_trace_raw #>
    2.12    register_config ML_Options.exception_debugger_raw #>
     3.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Aug 27 14:31:52 2018 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 27 14:42:24 2018 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature ML_COMPILER =
     3.5  sig
     3.6    type flags =
     3.7 -    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     3.8 +    {read: string option, write: string option, redirect: bool, verbose: bool,
     3.9        debug: bool option, writeln: string -> unit, warning: string -> unit}
    3.10    val debug_flags: bool option -> flags
    3.11    val flags: flags
    3.12 @@ -21,17 +21,17 @@
    3.13  (* flags *)
    3.14  
    3.15  type flags =
    3.16 -  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    3.17 +  {read: string option, write: string option, redirect: bool, verbose: bool,
    3.18      debug: bool option, writeln: string -> unit, warning: string -> unit};
    3.19  
    3.20  fun debug_flags opt_debug : flags =
    3.21 -  {SML = false, exchange = false, redirect = false, verbose = false,
    3.22 +  {read = NONE, write = NONE, redirect = false, verbose = false,
    3.23      debug = opt_debug, writeln = writeln, warning = warning};
    3.24  
    3.25  val flags = debug_flags NONE;
    3.26  
    3.27  fun verbose b (flags: flags) =
    3.28 -  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
    3.29 +  {read = #read flags, write = #write flags, redirect = #redirect flags, verbose = b,
    3.30      debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    3.31  
    3.32  
    3.33 @@ -154,14 +154,14 @@
    3.34      val opt_context = Context.get_generic_context ();
    3.35  
    3.36      val env as {debug, name_space, add_breakpoints} =
    3.37 -      (case (ML_Recursive.get (), #SML flags orelse #exchange flags) of
    3.38 +      (case (ML_Recursive.get (), is_some (#read flags) orelse is_some (#write flags)) of
    3.39          (SOME env, false) => env
    3.40        | _ =>
    3.41         {debug =
    3.42            (case #debug flags of
    3.43              SOME debug => debug
    3.44            | NONE => ML_Options.debugger_enabled opt_context),
    3.45 -        name_space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags},
    3.46 +        name_space = ML_Env.make_name_space {read = #read flags, write = #write flags},
    3.47          add_breakpoints = ML_Env.add_breakpoints});
    3.48  
    3.49  
    3.50 @@ -170,7 +170,7 @@
    3.51      val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    3.52  
    3.53      val input_explode =
    3.54 -      if #SML flags then String.explode
    3.55 +      if ML_Env.is_standard (ML_Env.default_env (#read flags)) then String.explode
    3.56        else maps (String.explode o Symbol.esc) o Symbol.explode;
    3.57  
    3.58      fun token_content tok =
     4.1 --- a/src/Pure/ML/ml_context.ML	Mon Aug 27 14:31:52 2018 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 14:42:24 2018 +0200
     4.3 @@ -195,7 +195,8 @@
     4.4    in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     4.5  
     4.6  fun eval_source flags source =
     4.7 -  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
     4.8 +  eval flags (Input.pos_of source)
     4.9 +    (ML_Lex.read_source (ML_Env.is_standard (ML_Env.default_env (#read flags))) source);
    4.10  
    4.11  fun eval_in ctxt flags pos ants =
    4.12    Context.setmp_generic_context (Option.map Context.Proof ctxt)
     5.1 --- a/src/Pure/ML/ml_env.ML	Mon Aug 27 14:31:52 2018 +0200
     5.2 +++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 14:42:24 2018 +0200
     5.3 @@ -7,16 +7,26 @@
     5.4  
     5.5  signature ML_ENV =
     5.6  sig
     5.7 +  val Isabelle: string
     5.8 +  val SML: string
     5.9 +  val is_standard: string -> bool
    5.10 +  val make_standard: bool -> string
    5.11 +  val ML_environment_raw: Config.raw
    5.12 +  val ML_environment: string Config.T
    5.13 +  val ML_read_global_raw: Config.raw
    5.14 +  val ML_read_global: bool Config.T
    5.15 +  val ML_write_global_raw: Config.raw
    5.16 +  val ML_write_global: bool Config.T
    5.17 +  val context_env: Context.generic -> string option -> string
    5.18 +  val default_env: string option -> string
    5.19    val inherit: Context.generic -> Context.generic -> Context.generic
    5.20 -  val forget_structure: string -> Context.generic -> Context.generic
    5.21 +  val setup: string -> theory -> theory
    5.22    val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
    5.23    val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
    5.24 -  val init_bootstrap: Context.generic -> Context.generic
    5.25 -  val SML_environment: bool Config.T
    5.26 -  val set_global: bool -> Context.generic -> Context.generic
    5.27 -  val restore_global: Context.generic -> Context.generic -> Context.generic
    5.28 -  val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
    5.29 -  val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    5.30 +  val forget_structure: string -> Context.generic -> Context.generic
    5.31 +  val bootstrap_name_space: Context.generic -> Context.generic
    5.32 +  val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
    5.33 +  val make_name_space: {read: string option, write: string option} -> ML_Name_Space.T
    5.34    val context: ML_Compiler0.context
    5.35    val name_space: ML_Name_Space.T
    5.36    val check_functor: string -> unit
    5.37 @@ -25,6 +35,39 @@
    5.38  structure ML_Env: ML_ENV =
    5.39  struct
    5.40  
    5.41 +(* named environments *)
    5.42 +
    5.43 +val Isabelle = "Isabelle";
    5.44 +val SML = "SML";
    5.45 +
    5.46 +fun is_standard env = env <> Isabelle;
    5.47 +fun make_standard sml = if sml then SML else Isabelle;
    5.48 +
    5.49 +val ML_environment_raw = Config.declare ("ML_environment", \<^here>) (fn _ => Config.String Isabelle);
    5.50 +val ML_environment = Config.string ML_environment_raw;
    5.51 +
    5.52 +fun context_env _ (SOME name) = name
    5.53 +  | context_env context NONE = Config.get_generic context ML_environment;
    5.54 +
    5.55 +fun default_env (SOME name) = name
    5.56 +  | default_env NONE =
    5.57 +      (case Context.get_generic_context () of
    5.58 +        NONE => Isabelle
    5.59 +      | SOME context => context_env context NONE);
    5.60 +
    5.61 +
    5.62 +(* global read/write *)
    5.63 +
    5.64 +val ML_read_global_raw = Config.declare ("ML_read_global", \<^here>) (fn _ => Config.Bool true);
    5.65 +val ML_write_global_raw = Config.declare ("ML_write_global", \<^here>) (fn _ => Config.Bool true);
    5.66 +
    5.67 +val ML_read_global = Config.bool ML_read_global_raw;
    5.68 +val ML_write_global = Config.bool ML_write_global_raw;
    5.69 +
    5.70 +fun read_global context = Config.get_generic context ML_read_global;
    5.71 +fun write_global context = Config.get_generic context ML_write_global;
    5.72 +
    5.73 +
    5.74  (* name space tables *)
    5.75  
    5.76  type tables =
    5.77 @@ -56,141 +99,120 @@
    5.78     Symtab.make ML_Name_Space.sml_signature,
    5.79     Symtab.make ML_Name_Space.sml_functor);
    5.80  
    5.81 -fun bootstrap_tables ((val1, type1, fixity1, structure1, signature1, functor1): tables) : tables =
    5.82 -  let
    5.83 -    val val2 =
    5.84 -      fold (fn (x, y) =>
    5.85 -        member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
    5.86 -      (#allVal ML_Name_Space.global ()) val1;
    5.87 -    val structure2 =
    5.88 -      fold (fn (x, y) =>
    5.89 -        member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
    5.90 -      (#allStruct ML_Name_Space.global ()) structure1;
    5.91 -    val signature2 =
    5.92 -      fold (fn (x, y) =>
    5.93 -        member (op =) ML_Name_Space.bootstrap_signatures x ? Symtab.update (x, y))
    5.94 -      (#allSig ML_Name_Space.global ()) signature1;
    5.95 -  in (val2, type1, fixity1, structure2, signature2, functor1) end;
    5.96 -
    5.97  
    5.98  (* context data *)
    5.99  
   5.100  type data =
   5.101 - {global: bool,
   5.102 -  tables: tables,
   5.103 -  sml_tables: tables,
   5.104 + {envs: tables Name_Space.table,
   5.105    breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table};
   5.106  
   5.107 -fun make_data (global, tables, sml_tables, breakpoints) : data =
   5.108 -  {global = global, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints};
   5.109 +fun make_data (envs, breakpoints) : data = {envs = envs, breakpoints = breakpoints};
   5.110  
   5.111 -structure Env = Generic_Data
   5.112 +structure Data = Generic_Data
   5.113  (
   5.114    type T = data
   5.115 -  val empty = make_data (true, empty_tables, sml_tables, Inttab.empty);
   5.116 -  fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
   5.117 +  val empty = make_data (Name_Space.empty_table "ML_environment", Inttab.empty);
   5.118 +  fun extend (data : T) = make_data (#envs data, #breakpoints data);
   5.119    fun merge (data : T * T) =
   5.120 -    make_data (false,
   5.121 -      merge_tables (apply2 #tables data),
   5.122 -      merge_tables (apply2 #sml_tables data),
   5.123 +    make_data ((apply2 #envs data) |> Name_Space.join_tables (K merge_tables),
   5.124        Inttab.merge (K true) (apply2 #breakpoints data));
   5.125  );
   5.126  
   5.127 -val inherit = Env.put o Env.get;
   5.128 +val inherit = Data.put o Data.get;
   5.129  
   5.130 -fun forget_structure name =
   5.131 -  Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.132 +fun setup env_name thy =
   5.133 +  thy |> (Context.theory_map o Data.map) (fn {envs, breakpoints} =>
   5.134      let
   5.135 -      val _ = if global then ML_Name_Space.forget_structure name else ();
   5.136 -      val tables' =
   5.137 -        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
   5.138 -    in make_data (global, tables', sml_tables, breakpoints) end);
   5.139 -
   5.140 -val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
   5.141 +      val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
   5.142 +      val tables = if env_name = Isabelle then empty_tables else sml_tables;
   5.143 +      val (_, envs') = envs
   5.144 +        |> Name_Space.define (Context.Theory thy') true (Binding.name env_name, tables);
   5.145 +    in make_data (envs', breakpoints) end);
   5.146  
   5.147 -fun add_breakpoints more_breakpoints =
   5.148 -  if is_some (Context.get_generic_context ()) then
   5.149 -    Context.>>
   5.150 -      (Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.151 -        let val breakpoints' =
   5.152 -          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
   5.153 -        in make_data (global, tables, sml_tables, breakpoints') end))
   5.154 -  else ();
   5.155 -
   5.156 +val get_env = Name_Space.get o #envs o Data.get;
   5.157  
   5.158 -(* SML environment for Isabelle/ML *)
   5.159 -
   5.160 -val SML_environment =
   5.161 -  Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
   5.162 +fun update_env env_name f context = context |> Data.map (fn {envs, breakpoints} =>
   5.163 +  let
   5.164 +    val _ = Name_Space.get envs env_name;
   5.165 +    val envs' = Name_Space.map_table_entry env_name f envs;
   5.166 +  in make_data (envs', breakpoints) end);
   5.167  
   5.168 -fun sml_env SML =
   5.169 -  SML orelse
   5.170 -    (case Context.get_generic_context () of
   5.171 -      NONE => false
   5.172 -    | SOME context => Config.get_generic context SML_environment);
   5.173 +fun forget_structure name context =
   5.174 +  (if write_global context then ML_Name_Space.forget_structure name else ();
   5.175 +    context |> update_env Isabelle (fn tables =>
   5.176 +      (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables)));
   5.177  
   5.178  
   5.179  (* name space *)
   5.180  
   5.181 -val init_bootstrap =
   5.182 -  Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.183 -    make_data (global, tables, bootstrap_tables sml_tables, breakpoints));
   5.184 +val bootstrap_name_space =
   5.185 +  update_env Isabelle (fn (tables: tables) =>
   5.186 +    let
   5.187 +      fun update entries (x, y) = member (op =) entries x ? Symtab.update (x, y);
   5.188 +      val bootstrap_val = update ML_Name_Space.bootstrap_values;
   5.189 +      val bootstrap_structure = update ML_Name_Space.bootstrap_structures;
   5.190 +      val bootstrap_signature = update ML_Name_Space.bootstrap_signatures;
   5.191  
   5.192 -fun set_global global =
   5.193 -  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
   5.194 -    make_data (global, tables, sml_tables, breakpoints));
   5.195 +      val (val1, type1, fixity1, structure1, signature1, functor1) = sml_tables;
   5.196 +      val val2 = val1
   5.197 +        |> fold bootstrap_val (#allVal ML_Name_Space.global ())
   5.198 +        |> Symtab.fold bootstrap_val (#1 tables);
   5.199 +      val structure2 = structure1
   5.200 +        |> fold bootstrap_structure (#allStruct ML_Name_Space.global ())
   5.201 +        |> Symtab.fold bootstrap_structure (#4 tables);
   5.202 +      val signature2 = signature1
   5.203 +        |> fold bootstrap_signature (#allSig ML_Name_Space.global ())
   5.204 +        |> Symtab.fold bootstrap_signature (#5 tables);
   5.205 +    in (val2, type1, fixity1, structure2, signature2, functor1) end);
   5.206  
   5.207 -val restore_global = set_global o #global o Env.get;
   5.208 -
   5.209 -fun add_name_space {SML} (space: ML_Name_Space.T) =
   5.210 -  Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.211 +fun add_name_space env (space: ML_Name_Space.T) =
   5.212 +  update_env env (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   5.213      let
   5.214 -      val (tables', sml_tables') =
   5.215 -        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
   5.216 -          (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
   5.217 -            let
   5.218 -              val val2 = fold Symtab.update (#allVal space ()) val1;
   5.219 -              val type2 = fold Symtab.update (#allType space ()) type1;
   5.220 -              val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
   5.221 -              val structure2 = fold Symtab.update (#allStruct space ()) structure1;
   5.222 -              val signature2 = fold Symtab.update (#allSig space ()) signature1;
   5.223 -              val functor2 = fold Symtab.update (#allFunct space ()) functor1;
   5.224 -            in (val2, type2, fixity2, structure2, signature2, functor2) end);
   5.225 -    in make_data (global, tables', sml_tables', breakpoints) end);
   5.226 +      val val2 = fold Symtab.update (#allVal space ()) val1;
   5.227 +      val type2 = fold Symtab.update (#allType space ()) type1;
   5.228 +      val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
   5.229 +      val structure2 = fold Symtab.update (#allStruct space ()) structure1;
   5.230 +      val signature2 = fold Symtab.update (#allSig space ()) signature1;
   5.231 +      val functor2 = fold Symtab.update (#allFunct space ()) functor1;
   5.232 +    in (val2, type2, fixity2, structure2, signature2, functor2) end);
   5.233 +
   5.234 +fun make_name_space {read, write} : ML_Name_Space.T =
   5.235 +  let
   5.236 +    val read_env = default_env read;
   5.237 +    val write_env = default_env write;
   5.238  
   5.239 -fun make_name_space {SML, exchange} : ML_Name_Space.T =
   5.240 -  let
   5.241 +    fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_env context read_env)) name;
   5.242 +    fun dest_env sel1 context = Symtab.dest (sel1 (get_env context read_env));
   5.243 +    fun enter_env ap1 entry = update_env write_env (ap1 (Symtab.update entry));
   5.244 +
   5.245      fun lookup sel1 sel2 name =
   5.246 -      if sml_env SML then
   5.247 -        Context.the_generic_context ()
   5.248 -        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
   5.249 -      else
   5.250 -        Context.get_generic_context ()
   5.251 -        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   5.252 -        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   5.253 +      if read_env = Isabelle then
   5.254 +        (case Context.get_generic_context () of
   5.255 +          NONE => sel2 ML_Name_Space.global name
   5.256 +        | SOME context =>
   5.257 +            (case lookup_env sel1 context name of
   5.258 +              NONE => if read_global context then sel2 ML_Name_Space.global name else NONE
   5.259 +            | some => some))
   5.260 +      else lookup_env sel1 (Context.the_generic_context ()) name;
   5.261  
   5.262      fun all sel1 sel2 () =
   5.263 -      (if sml_env SML then
   5.264 -        Context.the_generic_context ()
   5.265 -        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
   5.266 -      else
   5.267 -        Context.get_generic_context ()
   5.268 -        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   5.269 -        |> append (sel2 ML_Name_Space.global ()))
   5.270 -      |> sort_distinct (string_ord o apply2 #1);
   5.271 +      sort_distinct (string_ord o apply2 #1)
   5.272 +        (if read_env = Isabelle then
   5.273 +          (case Context.get_generic_context () of
   5.274 +            NONE => sel2 ML_Name_Space.global ()
   5.275 +          | SOME context =>
   5.276 +              dest_env sel1 context @
   5.277 +              (if read_global context then sel2 ML_Name_Space.global () else []))
   5.278 +         else dest_env sel1 (Context.the_generic_context ()));
   5.279  
   5.280      fun enter ap1 sel2 entry =
   5.281 -      if sml_env SML <> exchange then
   5.282 -        Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.283 -          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
   5.284 -          in make_data (global, tables, sml_tables', breakpoints) end))
   5.285 -      else if is_some (Context.get_generic_context ()) then
   5.286 -        Context.>> (Env.map (fn {global, tables, sml_tables, breakpoints} =>
   5.287 -          let
   5.288 -            val _ = if global then sel2 ML_Name_Space.global entry else ();
   5.289 -            val tables' = ap1 (Symtab.update entry) tables;
   5.290 -          in make_data (global, tables', sml_tables, breakpoints) end))
   5.291 -      else sel2 ML_Name_Space.global entry;
   5.292 +      if write_env = Isabelle then
   5.293 +        (case Context.get_generic_context () of
   5.294 +          NONE => sel2 ML_Name_Space.global entry
   5.295 +        | SOME context =>
   5.296 +            (if write_global context then sel2 ML_Name_Space.global entry else ();
   5.297 +             Context.>> (enter_env ap1 entry)))
   5.298 +      else Context.>> (enter_env ap1 entry);
   5.299    in
   5.300     {lookupVal    = lookup #1 #lookupVal,
   5.301      lookupType   = lookup #2 #lookupType,
   5.302 @@ -213,7 +235,7 @@
   5.303    end;
   5.304  
   5.305  val context: ML_Compiler0.context =
   5.306 - {name_space = make_name_space {SML = false, exchange = false},
   5.307 + {name_space = make_name_space {read = NONE, write = NONE},
   5.308    print_depth = NONE,
   5.309    here = Position.here oo Position.line_file,
   5.310    print = writeln,
   5.311 @@ -227,4 +249,20 @@
   5.312    if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
   5.313    else error ("Unknown ML functor: " ^ quote name);
   5.314  
   5.315 +
   5.316 +(* breakpoints *)
   5.317 +
   5.318 +val get_breakpoint = Inttab.lookup o #breakpoints o Data.get;
   5.319 +
   5.320 +fun add_breakpoints more_breakpoints =
   5.321 +  if is_some (Context.get_generic_context ()) then
   5.322 +    Context.>>
   5.323 +      (Data.map (fn {envs, breakpoints} =>
   5.324 +        let val breakpoints' =
   5.325 +          fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints;
   5.326 +        in make_data (envs, breakpoints') end))
   5.327 +  else ();
   5.328 +
   5.329  end;
   5.330 +
   5.331 +Theory.setup (ML_Env.setup ML_Env.Isabelle #> ML_Env.setup ML_Env.SML);
     6.1 --- a/src/Pure/ML/ml_file.ML	Mon Aug 27 14:31:52 2018 +0200
     6.2 +++ b/src/Pure/ML/ml_file.ML	Mon Aug 27 14:42:24 2018 +0200
     6.3 @@ -6,6 +6,8 @@
     6.4  
     6.5  signature ML_FILE =
     6.6  sig
     6.7 +  val command: string option -> bool option -> (theory -> Token.file list) ->
     6.8 +    Toplevel.transition -> Toplevel.transition
     6.9    val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    6.10    val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    6.11  end;
    6.12 @@ -13,7 +15,7 @@
    6.13  structure ML_File: ML_FILE =
    6.14  struct
    6.15  
    6.16 -fun command SML debug files = Toplevel.generic_theory (fn gthy =>
    6.17 +fun command env debug files = Toplevel.generic_theory (fn gthy =>
    6.18    let
    6.19      val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
    6.20      val provide = Resources.provide (src_path, digest);
    6.21 @@ -21,8 +23,8 @@
    6.22  
    6.23      val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
    6.24  
    6.25 -    val flags =
    6.26 -      {SML = SML, exchange = false, redirect = true, verbose = true,
    6.27 +    val flags: ML_Compiler.flags =
    6.28 +      {read = env, write = env, redirect = true, verbose = true,
    6.29          debug = debug, writeln = writeln, warning = warning};
    6.30    in
    6.31      gthy
    6.32 @@ -31,7 +33,7 @@
    6.33      |> Context.mapping provide (Local_Theory.background_theory provide)
    6.34    end);
    6.35  
    6.36 -val ML = command false;
    6.37 -val SML = command true;
    6.38 +val ML = command NONE;
    6.39 +val SML = command (SOME ML_Env.SML);
    6.40  
    6.41  end;
     7.1 --- a/src/Pure/ML_Bootstrap.thy	Mon Aug 27 14:31:52 2018 +0200
     7.2 +++ b/src/Pure/ML_Bootstrap.thy	Mon Aug 27 14:42:24 2018 +0200
     7.3 @@ -11,35 +11,37 @@
     7.4  external_file "$POLYML_EXE"
     7.5  
     7.6  
     7.7 -subsection \<open>Standard ML environment for virtual bootstrap\<close>
     7.8 +subsection \<open>ML environment for virtual bootstrap\<close>
     7.9  
    7.10 -setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
    7.11 -
    7.12 -SML_import \<open>
    7.13 +ML \<open>
    7.14 +  #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
    7.15 +    if member (op =) ML_Name_Space.hidden_structures name then
    7.16 +      ML (Input.string ("structure " ^ name ^ " = " ^ name))
    7.17 +    else ());
    7.18    structure Output_Primitives = Output_Primitives_Virtual;
    7.19    structure Thread_Data = Thread_Data_Virtual;
    7.20 +  structure PolyML = PolyML;
    7.21    fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
    7.22  \<close>
    7.23  
    7.24  
    7.25 -subsection \<open>Final setup of global ML environment\<close>
    7.26 +subsection \<open>Global ML environment for Isabelle/Pure\<close>
    7.27  
    7.28  ML \<open>Proofterm.proofs := 0\<close>
    7.29  
    7.30 -ML_export \<open>
    7.31 -  List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
    7.32 -  structure PolyML =
    7.33 -  struct
    7.34 -    val pointerEq = pointer_eq;
    7.35 -    structure IntInf = PolyML.IntInf;
    7.36 -  end;
    7.37 +ML \<open>
    7.38 +  Context.setmp_generic_context NONE
    7.39 +    ML \<open>
    7.40 +      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
    7.41 +      structure PolyML =
    7.42 +      struct
    7.43 +        val pointerEq = pointer_eq;
    7.44 +        structure IntInf = PolyML.IntInf;
    7.45 +      end;
    7.46 +    \<close>
    7.47  \<close>
    7.48  
    7.49 -ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
    7.50 -
    7.51 -
    7.52 -subsection \<open>Switch to bootstrap environment\<close>
    7.53 -
    7.54 -setup \<open>Config.put_global ML_Env.SML_environment true\<close>
    7.55 +setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
    7.56 +declare [[ML_read_global = false]]
    7.57  
    7.58  end
     8.1 --- a/src/Pure/Pure.thy	Mon Aug 27 14:31:52 2018 +0200
     8.2 +++ b/src/Pure/Pure.thy	Mon Aug 27 14:42:24 2018 +0200
     8.3 @@ -170,7 +170,7 @@
     8.4      (Parse.ML_source >> (fn source =>
     8.5        let
     8.6          val flags: ML_Compiler.flags =
     8.7 -          {SML = true, exchange = true, redirect = false, verbose = true,
     8.8 +          {read = SOME ML_Env.SML, write = NONE, redirect = false, verbose = true,
     8.9              debug = NONE, writeln = writeln, warning = warning};
    8.10        in
    8.11          Toplevel.theory
    8.12 @@ -182,7 +182,7 @@
    8.13      (Parse.ML_source >> (fn source =>
    8.14        let
    8.15          val flags: ML_Compiler.flags =
    8.16 -          {SML = false, exchange = true, redirect = false, verbose = true,
    8.17 +          {read = NONE, write = SOME ML_Env.SML, redirect = false, verbose = true,
    8.18              debug = NONE, writeln = writeln, warning = warning};
    8.19        in
    8.20          Toplevel.generic_theory
    8.21 @@ -196,10 +196,11 @@
    8.22      (Parse.ML_source >> (fn source =>
    8.23        Toplevel.generic_theory (fn context =>
    8.24          context
    8.25 -        |> ML_Env.set_global true
    8.26 +        |> Config.put_generic ML_Env.ML_write_global true
    8.27          |> ML_Context.exec (fn () =>
    8.28              ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
    8.29 -        |> ML_Env.restore_global context
    8.30 +        |> Config.put_generic ML_Env.ML_write_global
    8.31 +            (Config.get_generic context ML_Env.ML_write_global)
    8.32          |> Local_Theory.propagate_ml_env)));
    8.33  
    8.34  val _ =
    8.35 @@ -1440,4 +1441,6 @@
    8.36    qed
    8.37  qed
    8.38  
    8.39 +declare [[ML_write_global = false]]
    8.40 +
    8.41  end
     9.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 27 14:31:52 2018 +0200
     9.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 14:42:24 2018 +0200
     9.3 @@ -132,15 +132,17 @@
     9.4      "Context.put_generic_context (SOME ML_context)"];
     9.5  
     9.6  fun evaluate {SML, verbose} =
     9.7 -  ML_Context.eval
     9.8 -    {SML = SML, exchange = false, redirect = false, verbose = verbose,
     9.9 -      debug = SOME false, writeln = writeln_message, warning = warning_message}
    9.10 -    Position.none;
    9.11 +  let val env = ML_Env.make_standard SML in
    9.12 +    ML_Context.eval
    9.13 +      {read = SOME env, write = SOME env, redirect = false, verbose = verbose,
    9.14 +        debug = SOME false, writeln = writeln_message, warning = warning_message}
    9.15 +      Position.none
    9.16 +  end;
    9.17  
    9.18  fun eval_setup thread_name index SML context =
    9.19    context
    9.20    |> Context_Position.set_visible_generic false
    9.21 -  |> ML_Env.add_name_space {SML = SML}
    9.22 +  |> ML_Env.add_name_space (ML_Env.make_standard SML)
    9.23        (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
    9.24  
    9.25  fun eval_context thread_name index SML toks =