1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Thu Dec 20 21:12:01 2007 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Thu Dec 20 21:12:02 2007 +0100
     1.3 @@ -23,29 +23,66 @@
     1.4      Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
     1.5    val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
     1.6    val serial: unit -> int
     1.7 +  val get_data: 'a Universal.tag -> 'a option
     1.8 +  val put_data: 'a Universal.tag * 'a -> unit
     1.9  end;
    1.10  
    1.11  structure Multithreading: MULTITHREADING =
    1.12  struct
    1.13  
    1.14 +(* options *)
    1.15 +
    1.16  val trace = ref (0: int);
    1.17  fun tracing _ _ = ();
    1.18  
    1.19  val available = false;
    1.20  val max_threads = ref (1: int);
    1.21  
    1.22 +
    1.23 +(* critical section *)
    1.24 +
    1.25  fun self_critical () = false;
    1.26  fun NAMED_CRITICAL _ e = e ();
    1.27  fun CRITICAL e = e ();
    1.28  
    1.29 +
    1.30 +(* scheduling *)
    1.31 +
    1.32  datatype 'a task =
    1.33    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.34  
    1.35  fun schedule _ _ _ = raise Fail "No multithreading support";
    1.36  
    1.37 +
    1.38 +(* serial numbers *)
    1.39 +
    1.40  local val count = ref (0: int)
    1.41  in fun serial () = (count := ! count + 1; ! count) end;
    1.42  
    1.43 +
    1.44 +(* thread data *)
    1.45 +
    1.46 +local
    1.47 +
    1.48 +val data = ref ([]: Universal.universal ref list);
    1.49 +
    1.50 +fun find_data tag =
    1.51 +  let
    1.52 +    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
    1.53 +      | find [] = NONE;
    1.54 +  in find (! data) end;
    1.55 +
    1.56 +in
    1.57 +
    1.58 +fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
    1.59 +
    1.60 +fun put_data (tag, x) =
    1.61 +  (case find_data tag of
    1.62 +    SOME r => r := Universal.tagInject tag x
    1.63 +  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
    1.64 +
    1.65 +end;
    1.66 +
    1.67  end;
    1.68  
    1.69  structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;