src/Pure/Concurrent/thread_data.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
child 62890 728aa05e9433
permissions -rw-r--r--
clarified modules;
tuned signature;
wenzelm@62889
     1
(*  Title:      Pure/Concurrent/thread_data.ML
wenzelm@62889
     2
    Author:     Makarius
wenzelm@62889
     3
wenzelm@62889
     4
Thread-local data -- raw version without context management.
wenzelm@62889
     5
*)
wenzelm@62889
     6
wenzelm@62889
     7
signature THREAD_DATA =
wenzelm@62889
     8
sig
wenzelm@62889
     9
  type 'a var
wenzelm@62889
    10
  val var: unit -> 'a var
wenzelm@62889
    11
  val get: 'a var -> 'a option
wenzelm@62889
    12
  val put: 'a var -> 'a option -> unit
wenzelm@62889
    13
  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
wenzelm@62889
    14
end;
wenzelm@62889
    15
wenzelm@62889
    16
structure Thread_Data: THREAD_DATA =
wenzelm@62889
    17
struct
wenzelm@62889
    18
wenzelm@62889
    19
abstype 'a var = Var of 'a option Universal.tag
wenzelm@62889
    20
with
wenzelm@62889
    21
wenzelm@62889
    22
fun var () : 'a var = Var (Universal.tag ());
wenzelm@62889
    23
wenzelm@62889
    24
fun get (Var tag) =
wenzelm@62889
    25
  (case Thread.getLocal tag of
wenzelm@62889
    26
    SOME data => data
wenzelm@62889
    27
  | NONE => NONE);
wenzelm@62889
    28
wenzelm@62889
    29
fun put (Var tag) data = Thread.setLocal (tag, data);
wenzelm@62889
    30
wenzelm@62889
    31
fun setmp v data f x =
wenzelm@62889
    32
  uninterruptible (fn restore_attributes => fn () =>
wenzelm@62889
    33
    let
wenzelm@62889
    34
      val orig_data = get v;
wenzelm@62889
    35
      val _ = put v data;
wenzelm@62889
    36
      val result = Exn.capture (restore_attributes f) x;
wenzelm@62889
    37
      val _ = put v orig_data;
wenzelm@62889
    38
    in Exn.release result end) ();
wenzelm@62889
    39
wenzelm@62889
    40
end;
wenzelm@62889
    41
wenzelm@62889
    42
end;