--- a/src/Pure/ML/ml_name_space.ML Tue Apr 05 18:25:42 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Tue Apr 05 19:41:58 2016 +0200
@@ -58,17 +58,22 @@
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
- (* Standard ML name space *)
+ (* bootstrap environment *)
- val excluded_values = ["use", "exit"];
- val excluded_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+ val bootstrap_values =
+ ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+ val bootstrap_structures =
+ ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+
+
+ (* Standard ML environment *)
val sml_val =
- List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_values) (#allVal global ());
+ List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
val sml_type = #allType global ();
val sml_fixity = #allFix global ();
val sml_structure =
- List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_structures) (#allStruct global ());
+ List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
val sml_signature = #allSig global ();
val sml_functor = #allFunct global ();
end;