src/Pure/Concurrent/thread_data.ML
author wenzelm
Fri, 26 Apr 2024 13:25:44 +0200
changeset 80150 96f60533ec1d
parent 78720 909dc00766a0
permissions -rw-r--r--
update Windows test machines;

(*  Title:      Pure/Concurrent/thread_data.ML
    Author:     Makarius

Thread-local data -- physical version without context management.
*)

signature THREAD_DATA =
sig
  type 'a var
  val var: unit -> 'a var
  val get: 'a var -> 'a option
  val put: 'a var -> 'a option -> unit
  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
  val is_virtual: bool
end;

structure Thread_Data: THREAD_DATA =
struct

abstype 'a var = Var of 'a option Universal.tag
with

fun var () : 'a var = Var (Universal.tag ());

fun get (Var tag) =
  (case Thread.Thread.getLocal tag of
    SOME data => data
  | NONE => NONE);

fun put (Var tag) data = Thread.Thread.setLocal (tag, data);

fun setmp v data f x =
  Thread_Attributes.uninterruptible_body (fn run =>
    let
      val orig_data = get v;
      val _ = put v data;
      val result = Exn.capture0 (run f) x;
      val _ = put v orig_data;
    in Exn.release result end);

end;

val is_virtual = false;

end;