# HG changeset patch
# User wenzelm
# Date 1535389968 -7200
# Node ID 877534be1930d8937373b06b3eb88f4751d9f199
# Parent  2e4df245754ebe751c4572fe68aaddea78937bae
explicit setup of operations: avoid hardwired stuff;

diff -r 2e4df245754e -r 877534be1930 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -169,14 +169,8 @@
 
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
-    val input_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 =
-      if ML_Lex.is_comment tok then NONE
-      else SOME (input_explode (ML_Lex.check_content_of tok), tok);
+    val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);
+    fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok);
 
     val input_buffer =
       Unsynchronized.ref (map_filter token_content toks);
diff -r 2e4df245754e -r 877534be1930 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -197,8 +197,8 @@
 fun eval_source 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;
+    val {read_source, ...} = ML_Env.operations opt_context (#environment flags);
+  in eval flags (Input.pos_of source) (read_source source) end;
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_generic_context (Option.map Context.Proof ctxt)
diff -r 2e4df245754e -r 877534be1930 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -9,8 +9,6 @@
 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
@@ -18,12 +16,18 @@
   val ML_write_global_raw: Config.raw
   val ML_write_global: bool Config.T
   val inherit: Context.generic -> Context.generic -> Context.generic
-  val setup: string -> theory -> theory
+  type operations =
+   {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
+    explode_token: ML_Lex.token -> char list}
   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 setup: string -> operations -> theory -> theory
+  val Isabelle_operations: operations
+  val SML_operations: operations
+  val operations: Context.generic option -> string -> operations
   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
@@ -43,9 +47,6 @@
 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;
 
@@ -96,34 +97,35 @@
 
 (* context data *)
 
+type operations =
+ {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
+  explode_token: ML_Lex.token -> char list};
+
+type env = tables * operations;
+
 structure Data = Generic_Data
 (
-  type T = tables Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
+  type T = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
   val empty: T = (Name_Space.empty_table "ML_environment", Inttab.empty);
   val extend = I;
   fun merge ((envs1, breakpoints1), (envs2, breakpoints2)) : T =
-    (Name_Space.join_tables (K merge_tables) (envs1, envs2),
-      Inttab.merge (K true) (breakpoints1, breakpoints2));
+    ((envs1, envs2) |> Name_Space.join_tables
+      (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
+     Inttab.merge (K true) (breakpoints1, breakpoints2));
 );
 
 val inherit = Data.put o Data.get;
 
-fun setup env_name thy =
-  thy |> (Context.theory_map o Data.map o apfst) (fn envs =>
-    let
-      val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
-      val tables = if env_name = Isabelle then empty_tables else sml_tables;
-    in #2 (Name_Space.define (Context.Theory thy') true (Binding.name env_name, tables) envs) end);
+val get_env = Name_Space.get o #1 o Data.get;
+val get_tables = #1 oo get_env;
 
-val get_env = Name_Space.get o #1 o Data.get;
-
-fun update_env env_name f context = context |> Data.map (apfst (fn envs =>
+fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs =>
   let val _ = Name_Space.get envs env_name;
-  in Name_Space.map_table_entry env_name f envs end));
+  in Name_Space.map_table_entry env_name (apfst f) envs end);
 
 fun forget_structure name context =
   (if write_global context then ML_Name_Space.forget_structure name else ();
-    context |> update_env Isabelle (fn tables =>
+    context |> update_tables Isabelle (fn tables =>
       (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables)));
 
 
@@ -161,10 +163,38 @@
 val SML_import = print_environment {read = Isabelle, write = SML};
 
 
+(* setup operations *)
+
+fun setup env_name ops thy =
+  thy |> (Context.theory_map o Data.map o apfst) (fn envs =>
+    let
+      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') =
+        Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
+    in envs' end);
+
+fun make_operations SML: operations =
+ {read_source = ML_Lex.read_source SML,
+  explode_token = ML_Lex.explode_content_of SML};
+
+val Isabelle_operations = make_operations false;
+val SML_operations = make_operations true;
+
+val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);
+
+fun operations opt_context environment =
+  let val env = #read (parse_environment opt_context environment) in
+    (case opt_context of
+      NONE => Isabelle_operations
+    | SOME context => #2 (get_env context env))
+  end;
+
+
 (* name space *)
 
 val bootstrap_name_space =
-  update_env Isabelle (fn (tables: tables) =>
+  update_tables 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;
@@ -184,7 +214,7 @@
     in (val2, type1, fixity1, structure2, signature2, functor1) end);
 
 fun add_name_space env (space: ML_Name_Space.T) =
-  update_env env (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
+  update_tables env (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
     let
       val val2 = fold Symtab.update (#allVal space ()) val1;
       val type2 = fold Symtab.update (#allType space ()) type1;
@@ -198,9 +228,9 @@
   let
     val {read, write} = parse_environment (Context.get_generic_context ()) environment;
 
-    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_env sel1 context name = Symtab.lookup (sel1 (get_tables context read)) name;
+    fun dest_env sel1 context = Symtab.dest (sel1 (get_tables context read));
+    fun enter_env ap1 entry = update_tables write (ap1 (Symtab.update entry));
 
     fun lookup sel1 sel2 name =
       if read = Isabelle then
@@ -279,5 +309,3 @@
   else ();
 
 end;
-
-Theory.setup (ML_Env.setup ML_Env.Isabelle #> ML_Env.setup ML_Env.SML);
diff -r 2e4df245754e -r 877534be1930 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -22,6 +22,7 @@
   val kind_of: token -> token_kind
   val content_of: token -> string
   val check_content_of: token -> string
+  val explode_content_of: bool -> token -> char list
   val flatten: token list -> string
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -127,6 +128,10 @@
     Error msg => error msg
   | _ => content_of tok);
 
+fun explode_content_of SML =
+  check_content_of #>
+  (if SML then String.explode else Symbol.explode #> maps (Symbol.esc #> String.explode));
+
 
 (* flatten *)
 
diff -r 2e4df245754e -r 877534be1930 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Aug 27 17:30:13 2018 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 19:12:48 2018 +0200
@@ -131,16 +131,18 @@
     "Context.put_generic_context (SOME (Context.Proof ML_context))",
     "Context.put_generic_context (SOME ML_context)"];
 
+fun make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle;
+
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {environment = ML_Env.make_standard SML, redirect = false, verbose = verbose,
+    {environment = make_environment 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
   |> Context_Position.set_visible_generic false
-  |> ML_Env.add_name_space (ML_Env.make_standard SML)
+  |> ML_Env.add_name_space (make_environment SML)
       (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
 
 fun eval_context thread_name index SML toks =