src/Pure/ML-Systems/ml_stack_polyml-5.6.ML
author immler
Tue, 22 Dec 2015 21:58:27 +0100
changeset 61915 e9812a95d108
parent 61794 4c232a2ddeab
permissions -rw-r--r--
theory for type of bounded linear functions; differentiation under the integral sign
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61794
4c232a2ddeab discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
wenzelm
parents: 60923
diff changeset
     1
(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.6.ML
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
diff changeset
     2
61794
4c232a2ddeab discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
wenzelm
parents: 60923
diff changeset
     3
Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
diff changeset
     4
*)
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
diff changeset
     5
60923
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
     6
signature ML_STACK =
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
     7
sig
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
     8
  val limit: int option -> Thread.threadAttribute list
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
     9
end;
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
diff changeset
    10
60923
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    11
structure ML_Stack: ML_STACK =
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    12
struct
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    13
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    14
fun limit m = [Thread.MaximumMLStack m];
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    15
020becec359c clarified modules;
wenzelm
parents: 59468
diff changeset
    16
end;