src/Pure/Concurrent/thread_position.ML
author wenzelm
Sat, 09 Apr 2016 14:52:10 +0200
changeset 62929 b92565f98206
child 62940 a03592aafadf
permissions -rw-r--r--
shared thread position for physical/virtual Pure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62929
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/thread_position.ML
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     3
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     4
Thread-local position information.
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     5
*)
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     6
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     7
signature THREAD_POSITION =
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     8
sig
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
     9
  val get: unit -> (string * string) list
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    10
  val setmp: (string * string) list -> ('a -> 'b) -> 'a -> 'b
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    11
end;
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    12
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    13
structure Thread_Position: THREAD_POSITION =
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    14
struct
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    15
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    16
val var = Thread_Data.var () : (string * string) list Thread_Data.var;
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    17
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    18
fun get () =
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    19
  (case Thread_Data.get var of
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    20
    NONE => []
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    21
  | SOME props => props);
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    22
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    23
fun setmp props f x =
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    24
  Thread_Data.setmp var (if List.null props then NONE else SOME props) f x;
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    25
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    26
end;