--- a/src/Pure/Concurrent/unsynchronized.ML Sat Apr 02 20:23:51 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Sat Apr 02 20:33:34 2016 +0200
@@ -28,3 +28,6 @@
in Exn.release result end) ();
end;
+
+val _ = ML_Name_Space.forget_val "ref";
+val _ = ML_Name_Space.forget_type "ref";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive.ML Sat Apr 02 20:33:34 2016 +0200
@@ -0,0 +1,22 @@
+(* Title: Pure/ML/ml_pervasive.ML
+ Author: Makarius
+
+Pervasive ML environment.
+*)
+
+val seconds = Time.fromReal;
+
+val _ =
+ List.app ML_Name_Space.forget_val
+ ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+val pointer_eq = PolyML.pointerEq;
+
+val error_depth = PolyML.error_depth;
+
+open Thread;
--- a/src/Pure/ROOT Sat Apr 02 20:23:51 2016 +0200
+++ b/src/Pure/ROOT Sat Apr 02 20:33:34 2016 +0200
@@ -112,6 +112,7 @@
"ML/ml_name_space.ML"
"ML/ml_options.ML"
"ML/ml_pp.ML"
+ "ML/ml_pervasive.ML"
"ML/ml_pretty.ML"
"ML/ml_profiling.ML"
"ML/ml_statistics.ML"
--- a/src/Pure/ROOT.ML Sat Apr 02 20:23:51 2016 +0200
+++ b/src/Pure/ROOT.ML Sat Apr 02 20:33:34 2016 +0200
@@ -6,6 +6,7 @@
use "ML/ml_system.ML";
use "ML/ml_name_space.ML";
+use "ML/ml_pervasive.ML";
if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
else use "ML/fixed_int_dummy.ML";
@@ -22,50 +23,16 @@
use "General/exn.ML";
-val seconds = Time.fromReal;
-
-open Thread;
use "Concurrent/multithreading.ML";
-
use "Concurrent/unsynchronized.ML";
-val _ = ML_Name_Space.forget_val "ref";
-val _ = ML_Name_Space.forget_type "ref";
-(* pervasive environment *)
-
-val _ =
- List.app ML_Name_Space.forget_val
- ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* ML runtime system *)
+(* ML system *)
use "ML/ml_heap.ML";
use "ML/ml_profiling.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-
-(* ML toplevel pretty printing *)
-
use "ML/ml_pretty.ML";
-
-val error_depth = PolyML.error_depth;
-
-
-(* ML compiler *)
-
use "ML/ml_compiler0.ML";
-
-
-(* ML debugger *)
-
use_no_debug "ML/ml_debugger.ML";