removed managed_process (cf. General/shell_process.ML);
--- a/src/Pure/ML-Systems/multithreading.ML Sat Feb 16 16:43:59 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Sat Feb 16 16:44:00 2008 +0100
@@ -19,7 +19,6 @@
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;
@@ -42,12 +41,6 @@
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;