# HG changeset patch
# User wenzelm
# Date 1439408319 -7200
# Node ID 020becec359c0adaf49b2f616d0851a6dfd6d036
# Parent  0607869c2ff3b1ab92ef0a6a462ae436627664f3
clarified modules;

diff -r 0607869c2ff3 -r 020becec359c src/Pure/Concurrent/simple_thread.ML
--- 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 =
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
--- 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 = [];
-
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
--- 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];
-
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/ml_stack_dummy.ML
--- /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;
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML
--- /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;
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/polyml.ML
--- 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";
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ML-Systems/smlnj.ML
--- 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;
diff -r 0607869c2ff3 -r 020becec359c src/Pure/ROOT
--- 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"