src/Pure/ML-Systems/multithreading.ML
author wenzelm
Mon Sep 24 13:53:26 2007 +0200 (2007-09-24)
changeset 24690 c661dae1070a
child 25704 df9c8074ff09
permissions -rw-r--r--
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm@24690
     1
(*  Title:      Pure/ML-Systems/multithreading.ML
wenzelm@24690
     2
    ID:         $Id$
wenzelm@24690
     3
    Author:     Makarius
wenzelm@24690
     4
wenzelm@24690
     5
Dummy implementation of multithreading interface.
wenzelm@24690
     6
*)
wenzelm@24690
     7
wenzelm@24690
     8
signature MULTITHREADING =
wenzelm@24690
     9
sig
wenzelm@24690
    10
  val trace: int ref
wenzelm@24690
    11
  val tracing: int -> (unit -> string) -> unit
wenzelm@24690
    12
  val available: bool
wenzelm@24690
    13
  val max_threads: int ref
wenzelm@24690
    14
  val self_critical: unit -> bool
wenzelm@24690
    15
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
wenzelm@24690
    16
  val CRITICAL: (unit -> 'a) -> 'a
wenzelm@24690
    17
  datatype 'a task =
wenzelm@24690
    18
    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
wenzelm@24690
    19
  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
wenzelm@24690
    20
end;
wenzelm@24690
    21
wenzelm@24690
    22
structure Multithreading: MULTITHREADING =
wenzelm@24690
    23
struct
wenzelm@24690
    24
wenzelm@24690
    25
val trace = ref (0: int);
wenzelm@24690
    26
fun tracing _ _ = ();
wenzelm@24690
    27
wenzelm@24690
    28
val available = false;
wenzelm@24690
    29
val max_threads = ref (1: int);
wenzelm@24690
    30
wenzelm@24690
    31
fun self_critical () = false;
wenzelm@24690
    32
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    33
fun CRITICAL e = e ();
wenzelm@24690
    34
wenzelm@24690
    35
datatype 'a task =
wenzelm@24690
    36
  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
wenzelm@24690
    37
wenzelm@24690
    38
fun schedule _ _ _ = raise Fail "No multithreading support";
wenzelm@24690
    39
wenzelm@24690
    40
end;
wenzelm@24690
    41
wenzelm@24690
    42
val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
wenzelm@24690
    43
val CRITICAL = Multithreading.CRITICAL;