author | wenzelm |
Tue, 24 Jul 2007 19:44:33 +0200 | |
changeset 23962 | e0358fac0541 |
parent 23960 | c07ae96cbfc4 |
child 23973 | b6ce6de5b700 |
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 |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
10 |
val number_of_threads: int ref |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
11 |
val self_critical: unit -> bool |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
12 |
val CRITICAL: (unit -> 'a) -> 'a |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
13 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
14 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
15 |
structure Multithreading: MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
16 |
struct |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
17 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
18 |
val number_of_threads = ref 0; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
19 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
20 |
fun self_critical () = false; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
21 |
fun CRITICAL e = e (); |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
22 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
23 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
24 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
25 |
val CRITICAL = Multithreading.CRITICAL; |