tuned signature;
authorwenzelm
Thu Mar 17 10:21:43 2016 +0100 (2016-03-17)
changeset 62657cdd6db02eae8
parent 62656 dfd6fe970503
child 62658 c27dabf438d6
tuned signature;
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_env.ML	Thu Mar 17 10:00:38 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_env.ML	Thu Mar 17 10:21:43 2016 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  fun forget_structure name =
     1.5    Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     1.6      let
     1.7 -      val _ = if bootstrap then ML_Name_Space.forget_global_structure name else ();
     1.8 +      val _ = if bootstrap then ML_Name_Space.forget_structure name else ();
     1.9        val tables' =
    1.10          (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
    1.11      in make_data (bootstrap, tables', sml_tables, breakpoints) end);
     2.1 --- a/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:00:38 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 17 10:21:43 2016 +0100
     2.3 @@ -10,16 +10,17 @@
     2.4  
     2.5    type T = PolyML.NameSpace.nameSpace;
     2.6    val global = PolyML.globalNameSpace;
     2.7 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
     2.8  
     2.9    type valueVal = Values.value;
    2.10    fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
    2.11    fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
    2.12    val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
    2.13 +  val forget_val = PolyML.Compiler.forgetValue;
    2.14  
    2.15    type typeVal = TypeConstrs.typeConstr;
    2.16    fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
    2.17    val initial_type = #allType global ();
    2.18 +  val forget_type = PolyML.Compiler.forgetType;
    2.19  
    2.20    type fixityVal = Infixes.fixity;
    2.21    fun displayFix (_: string, x) = Infixes.print x;
    2.22 @@ -28,6 +29,7 @@
    2.23    type structureVal = Structures.structureVal;
    2.24    fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
    2.25    val initial_structure = #allStruct global ();
    2.26 +  val forget_structure = PolyML.Compiler.forgetStructure;
    2.27  
    2.28    type signatureVal = Signatures.signatureVal;
    2.29    fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
     3.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 10:00:38 2016 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 10:21:43 2016 +0100
     3.3 @@ -28,20 +28,20 @@
     3.4  use "Concurrent/multithreading.ML";
     3.5  
     3.6  use "Concurrent/unsynchronized.ML";
     3.7 -val _ = PolyML.Compiler.forgetValue "ref";
     3.8 -val _ = PolyML.Compiler.forgetType "ref";
     3.9 +val _ = ML_Name_Space.forget_val "ref";
    3.10 +val _ = ML_Name_Space.forget_type "ref";
    3.11  
    3.12  
    3.13  (* pervasive environment *)
    3.14  
    3.15 -val _ = PolyML.Compiler.forgetValue "isSome";
    3.16 -val _ = PolyML.Compiler.forgetValue "getOpt";
    3.17 -val _ = PolyML.Compiler.forgetValue "valOf";
    3.18 -val _ = PolyML.Compiler.forgetValue "foldl";
    3.19 -val _ = PolyML.Compiler.forgetValue "foldr";
    3.20 -val _ = PolyML.Compiler.forgetValue "print";
    3.21 -val _ = PolyML.Compiler.forgetValue "explode";
    3.22 -val _ = PolyML.Compiler.forgetValue "concat";
    3.23 +val _ = ML_Name_Space.forget_val "isSome";
    3.24 +val _ = ML_Name_Space.forget_val "getOpt";
    3.25 +val _ = ML_Name_Space.forget_val "valOf";
    3.26 +val _ = ML_Name_Space.forget_val "foldl";
    3.27 +val _ = ML_Name_Space.forget_val "foldr";
    3.28 +val _ = ML_Name_Space.forget_val "print";
    3.29 +val _ = ML_Name_Space.forget_val "explode";
    3.30 +val _ = ML_Name_Space.forget_val "concat";
    3.31  
    3.32  val ord = SML90.ord;
    3.33  val chr = SML90.chr;