src/Pure/Concurrent/thread_data.ML
author Fabian Huch <huch@in.tum.de>
Thu, 06 Jun 2024 08:58:58 +0200
changeset 80258 60013c49cedc
parent 78720 909dc00766a0
permissions -rw-r--r--
more build manager page;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/thread_data.ML
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     3
62890
728aa05e9433 clarified bootstrap;
wenzelm
parents: 62889
diff changeset
     4
Thread-local data -- physical version without context management.
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     5
*)
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     6
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     7
signature THREAD_DATA =
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     8
sig
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
     9
  type 'a var
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    10
  val var: unit -> 'a var
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    11
  val get: 'a var -> 'a option
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    12
  val put: 'a var -> 'a option -> unit
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    13
  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
62890
728aa05e9433 clarified bootstrap;
wenzelm
parents: 62889
diff changeset
    14
  val is_virtual: bool
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    15
end;
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    16
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    17
structure Thread_Data: THREAD_DATA =
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    18
struct
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    19
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    20
abstype 'a var = Var of 'a option Universal.tag
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    21
with
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    22
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    23
fun var () : 'a var = Var (Universal.tag ());
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    24
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    25
fun get (Var tag) =
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62891
diff changeset
    26
  (case Thread.Thread.getLocal tag of
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    27
    SOME data => data
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    28
  | NONE => NONE);
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    29
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62891
diff changeset
    30
fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    31
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    32
fun setmp v data f x =
78720
909dc00766a0 clarified signature;
wenzelm
parents: 78716
diff changeset
    33
  Thread_Attributes.uninterruptible_body (fn run =>
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    34
    let
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    35
      val orig_data = get v;
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    36
      val _ = put v data;
78716
97dfba4405e3 tuned signature;
wenzelm
parents: 78715
diff changeset
    37
      val result = Exn.capture0 (run f) x;
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    38
      val _ = put v orig_data;
78720
909dc00766a0 clarified signature;
wenzelm
parents: 78716
diff changeset
    39
    in Exn.release result end);
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    40
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    41
end;
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    42
62890
728aa05e9433 clarified bootstrap;
wenzelm
parents: 62889
diff changeset
    43
val is_virtual = false;
728aa05e9433 clarified bootstrap;
wenzelm
parents: 62889
diff changeset
    44
62889
99c7f31615c2 clarified modules;
wenzelm
parents:
diff changeset
    45
end;