author | wenzelm |
Tue, 24 Jul 2007 22:53:48 +0200 | |
changeset 23973 | b6ce6de5b700 |
parent 23960 | c07ae96cbfc4 |
child 23980 | d35dc9344515 |
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 |
23973 | 10 |
val max_threads: int ref |
23960
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 |
23973 | 13 |
val schedule: int -> ('a -> (unit -> unit) option * 'a) -> 'a -> exn list |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
14 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
15 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
16 |
structure Multithreading: MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
17 |
struct |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
18 |
|
23973 | 19 |
val max_threads = ref 1; |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
20 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
21 |
fun self_critical () = false; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
22 |
fun CRITICAL e = e (); |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
23 |
|
23973 | 24 |
fun schedule _ _ _ = raise Fail ("No multithreading support for " ^ ml_system); |
25 |
||
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
26 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
27 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
28 |
val CRITICAL = Multithreading.CRITICAL; |