# HG changeset patch # User wenzelm # Date 1459622014 -7200 # Node ID 2733b240bfeab3dd078ded9a617101d2ef55febb # Parent 744bfd770123199964a09afc9c9db83ece8edc50 clarified modules; diff -r 744bfd770123 -r 2733b240bfea src/Pure/Concurrent/unsynchronized.ML --- 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"; diff -r 744bfd770123 -r 2733b240bfea src/Pure/ML/ml_pervasive.ML --- /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; diff -r 744bfd770123 -r 2733b240bfea src/Pure/ROOT --- 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" diff -r 744bfd770123 -r 2733b240bfea src/Pure/ROOT.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";