src/Pure/ML-Systems/multithreading.ML
changeset 26074 44c5419cd9f1
parent 25775 90525e67ede7
child 26082 ea11278a0300
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Fri Feb 15 17:36:21 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Fri Feb 15 23:22:02 2008 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val available: bool
     1.5    val max_threads: int ref
     1.6    val max_threads_value: unit -> int
     1.7 +  val managed_process: string -> string * bool
     1.8    val self_critical: unit -> bool
     1.9    datatype 'a task =
    1.10      Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.11 @@ -41,6 +42,12 @@
    1.12  fun max_threads_value () = Int.max (! max_threads, 1);
    1.13  
    1.14  
    1.15 +(* managed external processes *)
    1.16 +
    1.17 +fun managed_process _ =
    1.18 +  raise Fail "No multithreading support -- cannot manage external processes";
    1.19 +
    1.20 +
    1.21  (* critical section *)
    1.22  
    1.23  fun self_critical () = false;
    1.24 @@ -53,7 +60,8 @@
    1.25  datatype 'a task =
    1.26    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.27  
    1.28 -fun schedule _ _ _ = raise Fail "No multithreading support";
    1.29 +fun schedule _ _ _ =
    1.30 +  raise Fail "No multithreading support -- cannot schedule tasks";
    1.31  
    1.32  
    1.33  (* serial numbers *)