# HG changeset patch
# User wenzelm
# Date 1459878118 -7200
# Node ID 5a0c0649197436b961fe75ed608a818423ef58ac
# Parent  b0194643e64cafa0b5bd18e4d53321f5d5439d67
clarified bootstrap environment;

diff -r b0194643e64c -r 5a0c06491974 NEWS
--- a/NEWS	Tue Apr 05 18:25:42 2016 +0200
+++ b/NEWS	Tue Apr 05 19:41:58 2016 +0200
@@ -235,7 +235,7 @@
 requiring separate files.
 
 * Low-level ML system structures (like PolyML and RunCall) are no longer
-exposed to Isabelle/ML user-space. The system option ML_system_unsafe
+exposed to Isabelle/ML user-space. The system option ML_system_bootstrap
 allows to override this for special test situations.
 
 * Antiquotation @{make_string} is available during Pure bootstrap --
diff -r b0194643e64c -r 5a0c06491974 etc/options
--- a/etc/options	Tue Apr 05 18:25:42 2016 +0200
+++ b/etc/options	Tue Apr 05 19:41:58 2016 +0200
@@ -126,8 +126,8 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
-option ML_system_unsafe : bool = false
-  -- "provide access to low-level ML system structures"
+option ML_system_bootstrap : bool = false
+  -- "provide access to low-level ML system structures (unsafe!)"
 
 
 section "Editor Reactivity"
diff -r b0194643e64c -r 5a0c06491974 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Apr 05 18:25:42 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 19:41:58 2016 +0200
@@ -101,11 +101,11 @@
             let
               val val2 =
                 fold (fn (x, y) =>
-                  member (op =) ML_Name_Space.excluded_values x ? Symtab.update (x, y))
+                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
                 (#allVal ML_Name_Space.global ()) val1;
               val structure2 =
                 fold (fn (x, y) =>
-                  member (op =) ML_Name_Space.excluded_structures x ? Symtab.update (x, y))
+                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
                 (#allStruct ML_Name_Space.global ()) structure1;
             in (val2, type1, fixity1, structure2, signature1, functor1) end);
     in make_data (bootstrap, tables, sml_tables', breakpoints) end);
diff -r b0194643e64c -r 5a0c06491974 src/Pure/ML/ml_name_space.ML
--- 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;
diff -r b0194643e64c -r 5a0c06491974 src/Pure/ML/ml_pervasive_final.ML
--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 18:25:42 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 19:41:58 2016 +0200
@@ -4,10 +4,11 @@
 Pervasive ML environment: final setup.
 *)
 
-if Options.default_bool "ML_system_unsafe" then ()
+if Options.default_bool "ML_system_bootstrap" then ()
 else
- (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.excluded_structures);
-  ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+  (List.app ML_Name_Space.forget_structure
+    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
diff -r b0194643e64c -r 5a0c06491974 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue Apr 05 18:25:42 2016 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 05 19:41:58 2016 +0200
@@ -215,7 +215,9 @@
   | name =>
       let val path = Path.explode name in
         (case try File.read path of
-          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
+          SOME s =>
+            (set_default (decode (YXML.parse_body s));
+             if default_bool "ML_system_bootstrap" then () else ignore (try File.rm path))
         | NONE => ())
       end);