(* Title: Pure/ML-Systems/multithreading.ML
ID: $Id$
Author: Makarius
Dummy implementation of multithreading setup.
*)
signature BASIC_MULTITHREADING =
sig
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
val CRITICAL: (unit -> 'a) -> 'a
end;
signature MULTITHREADING =
sig
include BASIC_MULTITHREADING
val trace: int ref
val tracing: int -> (unit -> string) -> unit
val available: bool
val max_threads: int ref
val max_threads_value: unit -> int
val no_interrupts: Thread.threadAttribute list
val sync_interrupts: Thread.threadAttribute list
val regular_interrupts: Thread.threadAttribute list
val with_attributes: Thread.threadAttribute list ->
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
val self_critical: unit -> bool
val serial: unit -> int
end;
structure Multithreading: MULTITHREADING =
struct
(* options *)
val trace = ref (0: int);
fun tracing _ _ = ();
val available = false;
val max_threads = ref (1: int);
fun max_threads_value () = Int.max (! max_threads, 1);
val no_interrupts = [];
val sync_interrupts = [];
val regular_interrupts = [];
fun with_attributes _ f x = f [] x;
(* critical section *)
fun self_critical () = false;
fun NAMED_CRITICAL _ e = e ();
fun CRITICAL e = e ();
(* serial numbers *)
local val count = ref (0: int)
in fun serial () = (count := ! count + 1; ! count) end;
end;
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
open BasicMultithreading;