src/Pure/ML-Systems/multithreading_dummy.ML
changeset 24207 402d629925ed
parent 24118 464f260e5a20
child 24593 1547ea587f5a
     1.1 --- a/src/Pure/ML-Systems/multithreading_dummy.ML	Thu Aug 09 19:19:23 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Thu Aug 09 23:53:49 2007 +0200
     1.3 @@ -5,13 +5,6 @@
     1.4  Compatibility file for ML systems without multithreading.
     1.5  *)
     1.6  
     1.7 -structure Task =
     1.8 -struct
     1.9 -  datatype task = Task of (unit -> unit) | Running | Finished;
    1.10 -  fun is_running Running = true | is_running _ = false;
    1.11 -  fun is_finished Finished = true | is_finished _ = false;
    1.12 -end;
    1.13 -
    1.14  signature MULTITHREADING =
    1.15  sig
    1.16    val trace: int ref
    1.17 @@ -21,7 +14,9 @@
    1.18    val self_critical: unit -> bool
    1.19    val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    1.20    val CRITICAL: (unit -> 'a) -> 'a
    1.21 -  val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list
    1.22 +  datatype 'a task =
    1.23 +    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.24 +  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    1.25  end;
    1.26  
    1.27  structure Multithreading: MULTITHREADING =
    1.28 @@ -37,6 +32,9 @@
    1.29  fun NAMED_CRITICAL _ e = e ();
    1.30  fun CRITICAL e = e ();
    1.31  
    1.32 +datatype 'a task =
    1.33 +  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.34 +
    1.35  fun schedule _ _ _ = raise Fail "No multithreading support";
    1.36  
    1.37  end;