hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
authorwenzelm
Thu Mar 17 10:54:28 2016 +0100 (2016-03-17)
changeset 62659bb29cc00c31f
parent 62658 c27dabf438d6
child 62660 285308563814
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
src/Pure/ML/ml_name_space.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:22:50 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:54:28 2016 +0100
     1.3 @@ -6,6 +6,8 @@
     1.4  
     1.5  structure ML_Name_Space =
     1.6  struct
     1.7 +  val critical_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
     1.8 +
     1.9    open PolyML.NameSpace;
    1.10  
    1.11    type T = PolyML.NameSpace.nameSpace;
    1.12 @@ -28,7 +30,9 @@
    1.13  
    1.14    type structureVal = Structures.structureVal;
    1.15    fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
    1.16 -  val initial_structure = #allStruct global ();
    1.17 +  val initial_structure =
    1.18 +    List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures))
    1.19 +      (#allStruct global ());
    1.20    val forget_structure = PolyML.Compiler.forgetStructure;
    1.21  
    1.22    type signatureVal = Signatures.signatureVal;
     2.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 10:22:50 2016 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 10:54:28 2016 +0100
     2.3 @@ -34,14 +34,9 @@
     2.4  
     2.5  (* pervasive environment *)
     2.6  
     2.7 -val _ = ML_Name_Space.forget_val "isSome";
     2.8 -val _ = ML_Name_Space.forget_val "getOpt";
     2.9 -val _ = ML_Name_Space.forget_val "valOf";
    2.10 -val _ = ML_Name_Space.forget_val "foldl";
    2.11 -val _ = ML_Name_Space.forget_val "foldr";
    2.12 -val _ = ML_Name_Space.forget_val "print";
    2.13 -val _ = ML_Name_Space.forget_val "explode";
    2.14 -val _ = ML_Name_Space.forget_val "concat";
    2.15 +val _ =
    2.16 +  List.app ML_Name_Space.forget_val
    2.17 +    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    2.18  
    2.19  val ord = SML90.ord;
    2.20  val chr = SML90.chr;
    2.21 @@ -165,6 +160,8 @@
    2.22  use "General/sha1_polyml.ML";
    2.23  use "General/sha1_samples.ML";
    2.24  
    2.25 +val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
    2.26 +
    2.27  use "PIDE/yxml.ML";
    2.28  use "PIDE/document_id.ML";
    2.29