# HG changeset patch
# User wenzelm
# Date 1186696429 -7200
# Node ID 402d629925ed9cfcdf2edd9686b22cb52003dee7
# Parent  9572c9374dc6aa99ad980783491ec0aaf52cae51
schedule: more precise task model;
removed obsolete structure Task;

diff -r 9572c9374dc6 -r 402d629925ed src/Pure/ML-Systems/multithreading_dummy.ML
--- a/src/Pure/ML-Systems/multithreading_dummy.ML	Thu Aug 09 19:19:23 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Thu Aug 09 23:53:49 2007 +0200
@@ -5,13 +5,6 @@
 Compatibility file for ML systems without multithreading.
 *)
 
-structure Task =
-struct
-  datatype task = Task of (unit -> unit) | Running | Finished;
-  fun is_running Running = true | is_running _ = false;
-  fun is_finished Finished = true | is_finished _ = false;
-end;
-
 signature MULTITHREADING =
 sig
   val trace: int ref
@@ -21,7 +14,9 @@
   val self_critical: unit -> bool
   val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
   val CRITICAL: (unit -> 'a) -> 'a
-  val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list
+  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 =
@@ -37,6 +32,9 @@
 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;