# HG changeset patch
# User wenzelm
# Date 1185375948 -7200
# Node ID d35dc9344515ebf65f5489467b4c429c77c6a627
# Parent  a15c13a54ab5fb017ea974a2ce4bc5216783f4d7
added structure Task;
added trace flag, official tracing operation;
added named CRITICAL';
schedule: tuned signature;

diff -r a15c13a54ab5 -r d35dc9344515 src/Pure/ML-Systems/multithreading_dummy.ML
--- a/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Jul 25 17:05:47 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Jul 25 17:05:48 2007 +0200
@@ -5,24 +5,41 @@
 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: bool ref
+  val tracing: (unit -> string) -> unit
+  val available: bool
   val max_threads: int ref
   val self_critical: unit -> bool
+  val CRITICAL': string -> (unit -> 'a) -> 'a
   val CRITICAL: (unit -> 'a) -> 'a
-  val schedule: int -> ('a -> (unit -> unit) option * 'a) -> 'a -> exn list
+  val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list
 end;
 
 structure Multithreading: MULTITHREADING =
 struct
 
+val trace = ref false;
+fun tracing _ = ();
+
+val available = false;
 val max_threads = ref 1;
 
 fun self_critical () = false;
+fun CRITICAL' _ e = e ();
 fun CRITICAL e = e ();
 
-fun schedule _ _ _ = raise Fail ("No multithreading support for " ^ ml_system);
+fun schedule _ _ _ = raise Fail "Multithreading support unavailable";
 
 end;
 
+val CRITICAL' = Multithreading.CRITICAL';
 val CRITICAL = Multithreading.CRITICAL;