# HG changeset patch
# User wenzelm
# Date 1459793228 -7200
# Node ID 07eea2843b82aad9b4dbc3e0e68ebb51d294764e
# Parent  1f1a2c33ccf4b9d1f2caeced3d7e7653cc340132
option ML_system_unsafe;

diff -r 1f1a2c33ccf4 -r 07eea2843b82 NEWS
--- a/NEWS	Mon Apr 04 19:48:54 2016 +0200
+++ b/NEWS	Mon Apr 04 20:07:08 2016 +0200
@@ -230,6 +230,10 @@
 
 *** ML ***
 
+* Low-level ML system structures (like PolyML and RunCall) are no longer
+exposed to Isabelle/ML user-space. The system option ML_system_unsafe
+allows to override this for special test situations.
+
 * Antiquotation @{make_string} is available during Pure bootstrap --
 with approximative output quality.
 
diff -r 1f1a2c33ccf4 -r 07eea2843b82 etc/options
--- a/etc/options	Mon Apr 04 19:48:54 2016 +0200
+++ b/etc/options	Mon Apr 04 20:07:08 2016 +0200
@@ -126,6 +126,9 @@
 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"
+
 
 section "Editor Reactivity"
 
diff -r 1f1a2c33ccf4 -r 07eea2843b82 src/Pure/ML/ml_final.ML
--- a/src/Pure/ML/ml_final.ML	Mon Apr 04 19:48:54 2016 +0200
+++ b/src/Pure/ML/ml_final.ML	Mon Apr 04 20:07:08 2016 +0200
@@ -4,9 +4,11 @@
 Final setup of ML environment.
 *)
 
-(*no access to system internals!*)
-structure PolyML = struct structure IntInf = PolyML.IntInf end;
-val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
+if Options.default_bool "ML_system_unsafe" then ()
+else
+  (List.app ML_Name_Space.forget_structure
+    ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
diff -r 1f1a2c33ccf4 -r 07eea2843b82 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Mon Apr 04 19:48:54 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Mon Apr 04 20:07:08 2016 +0200
@@ -66,8 +66,10 @@
   val sml_type = #allType global ();
   val sml_fixity = #allFix global ();
   val sml_structure =
-    List.filter (fn (a, _) => a <> "PolyML" andalso a <> "ML_System" andalso
-      not (List.exists (fn b => a = b) critical_structures)) (#allStruct global ());
+    List.filter (fn (a, _) =>
+      not (List.exists (fn b => a = b)
+        ["ML_System", "PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]))
+      (#allStruct global ());
   val sml_signature =
     List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
   val sml_functor = #allFunct global ();