author | wenzelm |
Mon, 24 Sep 2007 13:52:50 +0200 | |
changeset 24688 | a5754ca5c510 |
parent 24593 | 1547ea587f5a |
permissions | -rw-r--r-- |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/multithreading_dummy.ML |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
4 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
5 |
Compatibility file for ML systems without multithreading. |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
6 |
*) |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
7 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
8 |
signature MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
9 |
sig |
24118 | 10 |
val trace: int ref |
11 |
val tracing: int -> (unit -> string) -> unit |
|
23980 | 12 |
val available: bool |
23973 | 13 |
val max_threads: int ref |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
14 |
val self_critical: unit -> bool |
23990 | 15 |
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
16 |
val CRITICAL: (unit -> 'a) -> 'a |
24207 | 17 |
datatype 'a task = |
18 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
|
19 |
val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list |
|
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
20 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
21 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
22 |
structure Multithreading: MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
23 |
struct |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
24 |
|
24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24207
diff
changeset
|
25 |
val trace = ref (0: int); |
24118 | 26 |
fun tracing _ _ = (); |
23980 | 27 |
|
28 |
val available = false; |
|
24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24207
diff
changeset
|
29 |
val max_threads = ref (1: int); |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
30 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
31 |
fun self_critical () = false; |
23990 | 32 |
fun NAMED_CRITICAL _ e = e (); |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
33 |
fun CRITICAL e = e (); |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
34 |
|
24207 | 35 |
datatype 'a task = |
36 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
|
37 |
||
24059 | 38 |
fun schedule _ _ _ = raise Fail "No multithreading support"; |
23973 | 39 |
|
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
40 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
41 |
|
23990 | 42 |
val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
43 |
val CRITICAL = Multithreading.CRITICAL; |