# HG changeset patch
# User wenzelm
# Date 1459718928 -7200
# Node ID ea9f12e422c7526f4556476ccb1e70d39e6005c3
# Parent  c91ca9935280f04682157ec62c8b3480adce0bb0
clarified SML name space: no access to structure PolyML;

diff -r c91ca9935280 -r ea9f12e422c7 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Sun Apr 03 23:16:13 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Sun Apr 03 23:28:48 2016 +0200
@@ -57,12 +57,12 @@
   val empty =
     make_data (true,
       (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
-      (Symtab.make ML_Name_Space.initial_val,
-       Symtab.make ML_Name_Space.initial_type,
-       Symtab.make ML_Name_Space.initial_fixity,
-       Symtab.make ML_Name_Space.initial_structure,
-       Symtab.make ML_Name_Space.initial_signature,
-       Symtab.make ML_Name_Space.initial_functor),
+      (Symtab.make ML_Name_Space.sml_val,
+       Symtab.make ML_Name_Space.sml_type,
+       Symtab.make ML_Name_Space.sml_fixity,
+       Symtab.make ML_Name_Space.sml_structure,
+       Symtab.make ML_Name_Space.sml_signature,
+       Symtab.make ML_Name_Space.sml_functor),
       Inttab.empty);
   fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
   fun merge (data : T * T) =
diff -r c91ca9935280 -r ea9f12e422c7 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sun Apr 03 23:16:13 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sun Apr 03 23:28:48 2016 +0200
@@ -40,30 +40,35 @@
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-  val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
   val forget_val = PolyML.Compiler.forgetValue;
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-  val initial_type = #allType global ();
   val forget_type = PolyML.Compiler.forgetType;
 
   type fixityVal = Infixes.fixity;
   fun displayFix (_: string, x) = Infixes.print x;
-  val initial_fixity = #allFix global ();
 
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-  val initial_structure =
-    List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures))
-      (#allStruct global ());
   val forget_structure = PolyML.Compiler.forgetStructure;
 
   type signatureVal = Signatures.signatureVal;
   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-  val initial_signature = #allSig global ();
 
   type functorVal = Functors.functorVal;
   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-  val initial_functor = #allFunct global ();
+
+
+  (* Standard ML name space *)
+
+  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+  val sml_type = #allType global ();
+  val sml_fixity = #allFix global ();
+  val sml_structure =
+    List.filter (fn (a, _) => a <> "PolyML" andalso a <> "ML_System" andalso
+      not (List.exists (fn b => a = b) critical_structures)) (#allStruct global ());
+  val sml_signature =
+    List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
+  val sml_functor = #allFunct global ();
 end;