clarified modules;
authorwenzelm
Wed, 12 Aug 2015 21:38:39 +0200
changeset 60923 020becec359c
parent 60917 0607869c2ff3
child 60924 610794dff23c
clarified modules;
src/Pure/Concurrent/simple_thread.ML
src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
src/Pure/ML-Systems/ml_stack_dummy.ML
src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ROOT
--- a/src/Pure/Concurrent/simple_thread.ML	Wed Aug 12 13:56:46 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Aug 12 21:38:39 2015 +0200
@@ -49,7 +49,7 @@
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
-  maximum_ml_stack stack_limit @
+  ML_Stack.limit stack_limit @
   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun fork (params: params) body =
--- a/src/Pure/ML-Systems/maximum_ml_stack_dummy.ML	Wed Aug 12 13:56:46 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      Pure/ML-Systems/maximum_ml_stack_dummy.ML
-
-Maximum stack size (in words) for ML threads -- dummy version.
-*)
-
-fun maximum_ml_stack (_: int option) : Thread.threadAttribute list = [];
-
--- a/src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML	Wed Aug 12 13:56:46 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
-*)
-
-fun maximum_ml_stack limit = [Thread.MaximumMLStack limit];
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_stack_dummy.ML	Wed Aug 12 21:38:39 2015 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_stack_dummy.ML
+
+Maximum stack size (in words) for ML threads -- dummy version.
+*)
+
+signature ML_STACK =
+sig
+  val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit (_: int option) : Thread.threadAttribute list = [];
+
+end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML	Wed Aug 12 21:38:39 2015 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
+
+Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
+*)
+
+signature ML_STACK =
+sig
+  val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit m = [Thread.MaximumMLStack m];
+
+end;
--- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 12 13:56:46 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 12 21:38:39 2015 +0200
@@ -61,8 +61,8 @@
 use "ML-Systems/multithreading_polyml.ML";
 
 if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
-else use "ML-Systems/maximum_ml_stack_dummy.ML";
+then use "ML-Systems/ml_stack_polyml-5.5.3.ML"
+else use "ML-Systems/ml_stack_dummy.ML";
 
 use "ML-Systems/unsynchronized.ML";
 val _ = PolyML.Compiler.forgetValue "ref";
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Aug 12 13:56:46 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Aug 12 21:38:39 2015 +0200
@@ -18,7 +18,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
-use "ML-Systems/maximum_ml_stack_dummy.ML";
+use "ML-Systems/ml_stack_dummy.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/ml_name_space.ML";
 structure PolyML = struct end;
--- a/src/Pure/ROOT	Wed Aug 12 13:56:46 2015 +0200
+++ b/src/Pure/ROOT	Wed Aug 12 21:38:39 2015 +0200
@@ -6,8 +6,6 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/maximum_ml_stack_dummy.ML"
-    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -17,6 +15,8 @@
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_stack_dummy.ML"
+    "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
@@ -41,8 +41,6 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/maximum_ml_stack_dummy.ML"
-    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -52,6 +50,8 @@
     "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
+    "ML-Systems/ml_stack_dummy.ML"
+    "ML-Systems/ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"