(*  Title:      Pure/ML-Systems/multithreading.ML

    ID:         $Id$

    Author:     Makarius

Dummy implementation of multithreading interface.

*)

signature MULTITHREADING =

sig

  val trace: int ref

  val tracing: int -> (unit -> string) -> unit

  val available: bool

  val max_threads: int ref

  val self_critical: unit -> bool

  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a

  val CRITICAL: (unit -> 'a) -> 'a

  datatype 'a task =

    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;

  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list

end;

structure Multithreading: MULTITHREADING =

struct

val trace = ref (0: int);

fun tracing _ _ = ();

val available = false;

val max_threads = ref (1: int);

fun self_critical () = false;

fun NAMED_CRITICAL _ e = e ();

fun CRITICAL e = e ();

datatype 'a task =

  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;

fun schedule _ _ _ = raise Fail "No multithreading support";

end;

val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;

val CRITICAL = Multithreading.CRITICAL;