src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Fri Feb 15 17:36:21 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Fri Feb 15 23:22:02 2008 +0100
@@ -19,6 +19,7 @@
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
+  val managed_process: string -> string * bool
   val self_critical: unit -> bool
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
@@ -41,6 +42,12 @@
 fun max_threads_value () = Int.max (! max_threads, 1);
 
 
+(* managed external processes *)
+
+fun managed_process _ =
+  raise Fail "No multithreading support -- cannot manage external processes";
+
+
 (* critical section *)
 
 fun self_critical () = false;
@@ -53,7 +60,8 @@
 datatype 'a task =
   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
 
-fun schedule _ _ _ = raise Fail "No multithreading support";
+fun schedule _ _ _ =
+  raise Fail "No multithreading support -- cannot schedule tasks";
 
 
 (* serial numbers *)