# HG changeset patch # User wenzelm # Date 1535373744 -7200 # Node ID 5a53724fe24752e1f8e33becd1dbc6bfacf7f334 # Parent 6296915dee6e26c209b2d53e5352285a13fad2ec support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment; diff -r 6296915dee6e -r 5a53724fe247 src/FOL/IFOL.thy --- 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 \\<^assert> (not (can ML \open RunCall\))\ ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Provers/splitter.ML" ML_file "~~/src/Provers/hypsubst.ML" diff -r 6296915dee6e -r 5a53724fe247 src/Pure/Isar/attrib.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 #> diff -r 6296915dee6e -r 5a53724fe247 src/Pure/ML/ml_compiler.ML --- 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 = diff -r 6296915dee6e -r 5a53724fe247 src/Pure/ML/ml_context.ML --- 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) diff -r 6296915dee6e -r 5a53724fe247 src/Pure/ML/ml_env.ML --- 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); diff -r 6296915dee6e -r 5a53724fe247 src/Pure/ML/ml_file.ML --- 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; diff -r 6296915dee6e -r 5a53724fe247 src/Pure/ML_Bootstrap.thy --- 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 \Standard ML environment for virtual bootstrap\ +subsection \ML environment for virtual bootstrap\ -setup \Context.theory_map ML_Env.init_bootstrap\ - -SML_import \ +ML \ + #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) = (); \ -subsection \Final setup of global ML environment\ +subsection \Global ML environment for Isabelle/Pure\ ML \Proofterm.proofs := 0\ -ML_export \ - 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 \ + Context.setmp_generic_context NONE + ML \ + 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 \\<^assert> (not (can ML \open RunCall\))\ - - -subsection \Switch to bootstrap environment\ - -setup \Config.put_global ML_Env.SML_environment true\ +setup \Context.theory_map ML_Env.bootstrap_name_space\ +declare [[ML_read_global = false]] end diff -r 6296915dee6e -r 5a53724fe247 src/Pure/Pure.thy --- 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 diff -r 6296915dee6e -r 5a53724fe247 src/Pure/Tools/debugger.ML --- 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 =