src/Pure/ML-Systems/multithreading_dummy.ML
author wenzelm
Fri, 03 Aug 2007 22:33:09 +0200
changeset 24150 ed724867099a
parent 24118 464f260e5a20
child 24207 402d629925ed
permissions -rw-r--r--
sort indexes according to symbolic update_time (multithreading-safe);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
     8
structure Task =
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
     9
struct
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    10
  datatype task = Task of (unit -> unit) | Running | Finished;
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    11
  fun is_running Running = true | is_running _ = false;
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    12
  fun is_finished Finished = true | is_finished _ = false;
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    13
end;
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    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
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24059
diff changeset
    17
  val trace: int ref
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24059
diff changeset
    18
  val tracing: int -> (unit -> string) -> unit
23980
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    19
  val available: bool
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23960
diff changeset
    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
72a9b436af56 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23980
diff changeset
    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
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    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
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24059
diff changeset
    30
val trace = ref 0;
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24059
diff changeset
    31
fun tracing _ _ = ();
23980
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    32
d35dc9344515 added structure Task;
wenzelm
parents: 23973
diff changeset
    33
val available = false;
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23960
diff changeset
    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
72a9b436af56 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23980
diff changeset
    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
89a5382406a1 tuned msg;
wenzelm
parents: 23990
diff changeset
    40
fun schedule _ _ _ = raise Fail "No multithreading support";
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23960
diff changeset
    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
72a9b436af56 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23980
diff changeset
    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;