shared thread position for physical/virtual Pure;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_position.ML	Sat Apr 09 14:52:10 2016 +0200
@@ -0,0 +1,26 @@
+(*  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;

--- a/src/Pure/General/position.ML	Sat Apr 09 14:40:00 2016 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 09 14:52:10 2016 +0200
@@ -243,9 +243,8 @@
 
 (* thread data *)
 
-val thread_data_var = Thread_Data.var () : T Thread_Data.var;
-fun thread_data () = the_default none (Thread_Data.get thread_data_var);
-fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
+val thread_data = of_properties o Thread_Position.get;
+fun setmp_thread_data pos = Thread_Position.setmp (properties_of pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())

--- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:40:00 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:52:10 2016 +0200
@@ -65,9 +65,10 @@
       "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
   val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
   val bootstrap_structures =
-    ["Exn", "Basic_Exn", "Thread_Data", "ML_Recursive", "PolyML"] @ hidden_structures;
+    ["Exn", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive", "PolyML"] @
+      hidden_structures;
   val bootstrap_signatures =
-    ["EXN", "BASIC_EXN", "THREAD_DATA", "ML_RECURSIVE"];
+    ["EXN", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE"];
 
 
   (* Standard ML environment *)

--- a/src/Pure/ROOT0.ML	Sat Apr 09 14:40:00 2016 +0200
+++ b/src/Pure/ROOT0.ML	Sat Apr 09 14:52:10 2016 +0200
@@ -4,5 +4,6 @@
 
 ML_file "Concurrent/thread_attributes.ML";
 ML_file "Concurrent/thread_data.ML";
+ML_file "Concurrent/thread_position.ML";
 
 ML_file "ML/ml_recursive.ML";