clarified environment: allow "read>write" specification;

--- a/src/Pure/ML/ml_compiler.ML	Mon Aug 27 17:26:14 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {read: string option, write: string option, redirect: bool, verbose: bool,
+    {environment: string, 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 =
-  {read: string option, write: string option, redirect: bool, verbose: bool,
+  {environment: string, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {read = NONE, write = NONE, redirect = false, verbose = false,
+  {environment = "", redirect = false, verbose = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
-  {read = #read flags, write = #write flags, redirect = #redirect flags, verbose = b,
+  {environment = #environment flags, redirect = #redirect flags, verbose = b,
     debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
 
@@ -154,15 +154,15 @@
     val opt_context = Context.get_generic_context ();
 
     val env as {debug, name_space, add_breakpoints} =
-      (case (ML_Recursive.get (), is_some (#read flags) orelse is_some (#write flags)) of
+      (case (ML_Recursive.get (), #environment 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 {read = #read flags, write = #write flags},
-        add_breakpoints = ML_Env.add_breakpoints});
+         {debug =
+            (case #debug flags of
+              SOME debug => debug
+            | NONE => ML_Options.debugger_enabled opt_context),
+          name_space = ML_Env.make_name_space (#environment flags),
+          add_breakpoints = ML_Env.add_breakpoints});
 
 
     (* input *)
@@ -170,7 +170,8 @@
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_explode =
-      if ML_Env.is_standard (ML_Env.default_env (#read flags)) then String.explode
+      if ML_Env.is_standard (#read (ML_Env.parse_environment opt_context (#environment 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 17:26:14 2018 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -195,8 +195,10 @@
   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 (ML_Env.is_standard (ML_Env.default_env (#read flags))) source);
+  let
+    val opt_context = Context.get_generic_context ();
+    val SML = ML_Env.is_standard (#read (ML_Env.parse_environment opt_context (#environment flags)));
+  in eval flags (Input.pos_of source) (ML_Lex.read_source SML source) end;
 
 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 17:26:14 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -19,12 +19,15 @@
   val ML_write_global: bool Config.T
   val inherit: Context.generic -> Context.generic -> Context.generic
   val setup: string -> theory -> theory
-  val context_env: Context.generic -> string option -> string
-  val default_env: string option -> string
+  type environment = {read: string, write: string}
+  val parse_environment: Context.generic option -> string -> environment
+  val print_environment: environment -> string
+  val SML_export: string
+  val SML_import: string
   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 make_name_space: string -> ML_Name_Space.T
   val context: ML_Compiler0.context
   val name_space: ML_Name_Space.T
   val check_functor: string -> unit
@@ -126,23 +129,36 @@
 
 (* environment name *)
 
-fun check_env opt_context name =
-  (case opt_context of
-    NONE =>
-      if name = Isabelle then name
-      else error ("Bad ML environment name " ^ quote name ^ " -- no context")
-  | SOME context => if name = Isabelle then name else (get_env context name; name));
+type environment = {read: string, write: string};
+
+val separator = ">";
+
+fun parse_environment opt_context environment =
+  let
+    fun check name =
+      (case opt_context of
+        NONE =>
+          if name = Isabelle then name
+          else error ("Bad ML environment name " ^ quote name ^ " -- no context")
+      | SOME context => if name = Isabelle then name else (get_env context name; name));
 
-fun context_env context opt_name =
-  check_env (SOME context) (the_default (Config.get_generic context ML_environment) opt_name);
+    val spec =
+      if environment = "" then
+        (case opt_context of
+          NONE => Isabelle
+        | SOME context => Config.get_generic context ML_environment)
+      else environment;
+    val (read, write) =
+      (case space_explode separator spec of
+        [a] => (a, a)
+      | [a, b] => (a, b)
+      | _ => error ("Malformed ML environment specification: " ^ quote spec));
+  in {read = check read, write = check write} end;
 
-fun default_env opt_name =
-  let val opt_context = Context.get_generic_context () in
-    check_env opt_context
-      (case opt_name of
-        SOME name => name
-      | NONE => (case opt_context of NONE => Isabelle | SOME context => context_env context NONE))
-  end;
+fun print_environment {read, write} = read ^ separator ^ write;
+
+val SML_export = print_environment {read = SML, write = Isabelle};
+val SML_import = print_environment {read = Isabelle, write = SML};
 
 
 (* name space *)
@@ -178,17 +194,16 @@
       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 =
+fun make_name_space environment : ML_Name_Space.T =
   let
-    val read_env = default_env read;
-    val write_env = default_env write;
+    val {read, write} = parse_environment (Context.get_generic_context ()) environment;
 
-    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_env sel1 context name = Symtab.lookup (sel1 (get_env context read)) name;
+    fun dest_env sel1 context = Symtab.dest (sel1 (get_env context read));
+    fun enter_env ap1 entry = update_env write (ap1 (Symtab.update entry));
 
     fun lookup sel1 sel2 name =
-      if read_env = Isabelle then
+      if read = Isabelle then
         (case Context.get_generic_context () of
           NONE => sel2 ML_Name_Space.global name
         | SOME context =>
@@ -199,7 +214,7 @@
 
     fun all sel1 sel2 () =
       sort_distinct (string_ord o apply2 #1)
-        (if read_env = Isabelle then
+        (if read = Isabelle then
           (case Context.get_generic_context () of
             NONE => sel2 ML_Name_Space.global ()
           | SOME context =>
@@ -208,7 +223,7 @@
          else dest_env sel1 (Context.the_generic_context ()));
 
     fun enter ap1 sel2 entry =
-      if write_env = Isabelle then
+      if write = Isabelle then
         (case Context.get_generic_context () of
           NONE => sel2 ML_Name_Space.global entry
         | SOME context =>
@@ -237,7 +252,7 @@
   end;
 
 val context: ML_Compiler0.context =
- {name_space = make_name_space {read = NONE, write = NONE},
+ {name_space = make_name_space "",
   print_depth = NONE,
   here = Position.here oo Position.line_file,
   print = writeln,

--- a/src/Pure/ML/ml_file.ML	Mon Aug 27 17:26:14 2018 +0200
+++ b/src/Pure/ML/ml_file.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -6,7 +6,7 @@
 
 signature ML_FILE =
 sig
-  val command: string option -> bool option -> (theory -> Token.file list) ->
+  val command: string -> 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
@@ -15,7 +15,7 @@
 structure ML_File: ML_FILE =
 struct
 
-fun command env debug files = Toplevel.generic_theory (fn gthy =>
+fun command environment 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);
@@ -24,7 +24,7 @@
     val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
     val flags: ML_Compiler.flags =
-      {read = env, write = env, redirect = true, verbose = true,
+      {environment = environment, redirect = true, verbose = true,
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
@@ -33,7 +33,7 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command NONE;
-val SML = command (SOME ML_Env.SML);
+val ML = command "";
+val SML = command ML_Env.SML;
 
 end;

--- a/src/Pure/Pure.thy	Mon Aug 27 17:26:14 2018 +0200
+++ b/src/Pure/Pure.thy	Mon Aug 27 17:30:13 2018 +0200
@@ -170,7 +170,7 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {read = SOME ML_Env.SML, write = NONE, redirect = false, verbose = true,
+          {environment = ML_Env.SML_export, 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 =
-          {read = NONE, write = SOME ML_Env.SML, redirect = false, verbose = true,
+          {environment = ML_Env.SML_import, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory

--- a/src/Pure/Tools/debugger.ML	Mon Aug 27 17:26:14 2018 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -132,12 +132,10 @@
     "Context.put_generic_context (SOME ML_context)"];
 
 fun evaluate {SML, verbose} =
-  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;
+  ML_Context.eval
+    {environment = ML_Env.make_standard SML, redirect = false, verbose = verbose,
+      debug = SOME false, writeln = writeln_message, warning = warning_message}
+    Position.none;
 
 fun eval_setup thread_name index SML context =
   context