renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
authorwenzelm
Mon Sep 24 13:53:26 2007 +0200 (2007-09-24)
changeset 24690c661dae1070a
parent 24689 ac5b5a6155dd
child 24691 e7f46ee04809
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_dummy.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Mon Sep 24 13:53:26 2007 +0200
     1.3 @@ -0,0 +1,43 @@
     1.4 +(*  Title:      Pure/ML-Systems/multithreading.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Dummy implementation of multithreading interface.
     1.9 +*)
    1.10 +
    1.11 +signature MULTITHREADING =
    1.12 +sig
    1.13 +  val trace: int ref
    1.14 +  val tracing: int -> (unit -> string) -> unit
    1.15 +  val available: bool
    1.16 +  val max_threads: int ref
    1.17 +  val self_critical: unit -> bool
    1.18 +  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    1.19 +  val CRITICAL: (unit -> 'a) -> 'a
    1.20 +  datatype 'a task =
    1.21 +    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.22 +  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    1.23 +end;
    1.24 +
    1.25 +structure Multithreading: MULTITHREADING =
    1.26 +struct
    1.27 +
    1.28 +val trace = ref (0: int);
    1.29 +fun tracing _ _ = ();
    1.30 +
    1.31 +val available = false;
    1.32 +val max_threads = ref (1: int);
    1.33 +
    1.34 +fun self_critical () = false;
    1.35 +fun NAMED_CRITICAL _ e = e ();
    1.36 +fun CRITICAL e = e ();
    1.37 +
    1.38 +datatype 'a task =
    1.39 +  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.40 +
    1.41 +fun schedule _ _ _ = raise Fail "No multithreading support";
    1.42 +
    1.43 +end;
    1.44 +
    1.45 +val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.46 +val CRITICAL = Multithreading.CRITICAL;
     2.1 --- a/src/Pure/ML-Systems/multithreading_dummy.ML	Mon Sep 24 13:52:51 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,43 +0,0 @@
     2.4 -(*  Title:      Pure/ML-Systems/multithreading_dummy.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Makarius
     2.7 -
     2.8 -Compatibility file for ML systems without multithreading.
     2.9 -*)
    2.10 -
    2.11 -signature MULTITHREADING =
    2.12 -sig
    2.13 -  val trace: int ref
    2.14 -  val tracing: int -> (unit -> string) -> unit
    2.15 -  val available: bool
    2.16 -  val max_threads: int ref
    2.17 -  val self_critical: unit -> bool
    2.18 -  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    2.19 -  val CRITICAL: (unit -> 'a) -> 'a
    2.20 -  datatype 'a task =
    2.21 -    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    2.22 -  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    2.23 -end;
    2.24 -
    2.25 -structure Multithreading: MULTITHREADING =
    2.26 -struct
    2.27 -
    2.28 -val trace = ref (0: int);
    2.29 -fun tracing _ _ = ();
    2.30 -
    2.31 -val available = false;
    2.32 -val max_threads = ref (1: int);
    2.33 -
    2.34 -fun self_critical () = false;
    2.35 -fun NAMED_CRITICAL _ e = e ();
    2.36 -fun CRITICAL e = e ();
    2.37 -
    2.38 -datatype 'a task =
    2.39 -  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    2.40 -
    2.41 -fun schedule _ _ _ = raise Fail "No multithreading support";
    2.42 -
    2.43 -end;
    2.44 -
    2.45 -val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    2.46 -val CRITICAL = Multithreading.CRITICAL;