author | wenzelm |
Fri, 03 Aug 2007 22:33:09 +0200 | |
changeset 24150 | ed724867099a |
parent 24118 | 464f260e5a20 |
child 24207 | 402d629925ed |
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 |
|
23980 | 8 |
structure Task = |
9 |
struct |
|
10 |
datatype task = Task of (unit -> unit) | Running | Finished; |
|
11 |
fun is_running Running = true | is_running _ = false; |
|
12 |
fun is_finished Finished = true | is_finished _ = false; |
|
13 |
end; |
|
14 |
||
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
15 |
signature MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
16 |
sig |
24118 | 17 |
val trace: int ref |
18 |
val tracing: int -> (unit -> string) -> unit |
|
23980 | 19 |
val available: bool |
23973 | 20 |
val max_threads: int ref |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
21 |
val self_critical: unit -> bool |
23990 | 22 |
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
23 |
val CRITICAL: (unit -> 'a) -> 'a |
23980 | 24 |
val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
25 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
26 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
27 |
structure Multithreading: MULTITHREADING = |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
28 |
struct |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
29 |
|
24118 | 30 |
val trace = ref 0; |
31 |
fun tracing _ _ = (); |
|
23980 | 32 |
|
33 |
val available = false; |
|
23973 | 34 |
val max_threads = ref 1; |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
35 |
|
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
36 |
fun self_critical () = false; |
23990 | 37 |
fun NAMED_CRITICAL _ e = e (); |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
38 |
fun CRITICAL e = e (); |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
39 |
|
24059 | 40 |
fun schedule _ _ _ = raise Fail "No multithreading support"; |
23973 | 41 |
|
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
42 |
end; |
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
43 |
|
23990 | 44 |
val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; |
23960
c07ae96cbfc4
Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff
changeset
|
45 |
val CRITICAL = Multithreading.CRITICAL; |