# HG changeset patch
# User wenzelm
# Date 1460206330 -7200
# Node ID b92565f98206873558935d39b0427d206e5f49f1
# Parent  0953dec1fcb0c065b1ba476be477e1104bb53e0f
shared thread position for physical/virtual Pure;

diff -r 0953dec1fcb0 -r b92565f98206 src/Pure/Concurrent/thread_position.ML
--- /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;
diff -r 0953dec1fcb0 -r b92565f98206 src/Pure/General/position.ML
--- 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 ())
diff -r 0953dec1fcb0 -r b92565f98206 src/Pure/ML/ml_name_space.ML
--- 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 *)
diff -r 0953dec1fcb0 -r b92565f98206 src/Pure/ROOT0.ML
--- 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";