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;

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

Thread-local position information.
*)

signature THREAD_POSITION =
sig
  val get: unit -> (string * string) list
  val setmp: (string * string) list -> ('a -> 'b) -> 'a -> 'b
end;

structure Thread_Position: THREAD_POSITION =
struct

val var = Thread_Data.var () : (string * string) list Thread_Data.var;

fun get () =
  (case Thread_Data.get var of
    NONE => []
  | SOME props => props);

fun setmp props f x =
  Thread_Data.setmp var (if List.null props then NONE else SOME props) f x;

end;