# HG changeset patch
# User wenzelm
# Date 1458208468 -3600
# Node ID bb29cc00c31feb73189b1bb349204f8d01c3caf9
# Parent  c27dabf438d69df7ad486450f1784ccb9431b613
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;

diff -r c27dabf438d6 -r bb29cc00c31f src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:22:50 2016 +0100
+++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:54:28 2016 +0100
@@ -6,6 +6,8 @@
 
 structure ML_Name_Space =
 struct
+  val critical_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+
   open PolyML.NameSpace;
 
   type T = PolyML.NameSpace.nameSpace;
@@ -28,7 +30,9 @@
 
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-  val initial_structure = #allStruct global ();
+  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;
diff -r c27dabf438d6 -r bb29cc00c31f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 17 10:22:50 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 17 10:54:28 2016 +0100
@@ -34,14 +34,9 @@
 
 (* pervasive environment *)
 
-val _ = ML_Name_Space.forget_val "isSome";
-val _ = ML_Name_Space.forget_val "getOpt";
-val _ = ML_Name_Space.forget_val "valOf";
-val _ = ML_Name_Space.forget_val "foldl";
-val _ = ML_Name_Space.forget_val "foldr";
-val _ = ML_Name_Space.forget_val "print";
-val _ = ML_Name_Space.forget_val "explode";
-val _ = ML_Name_Space.forget_val "concat";
+val _ =
+  List.app ML_Name_Space.forget_val
+    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
 
 val ord = SML90.ord;
 val chr = SML90.chr;
@@ -165,6 +160,8 @@
 use "General/sha1_polyml.ML";
 use "General/sha1_samples.ML";
 
+val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
+
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";