shared thread position for physical/virtual Pure;
authorwenzelm
Sat Apr 09 14:52:10 2016 +0200 (2016-04-09)
changeset 62929b92565f98206
parent 62928 0953dec1fcb0
child 62930 51ac6bc389e8
shared thread position for physical/virtual Pure;
src/Pure/Concurrent/thread_position.ML
src/Pure/General/position.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ROOT0.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/thread_position.ML	Sat Apr 09 14:52:10 2016 +0200
     1.3 @@ -0,0 +1,26 @@
     1.4 +(*  Title:      Pure/Concurrent/thread_position.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Thread-local position information.
     1.8 +*)
     1.9 +
    1.10 +signature THREAD_POSITION =
    1.11 +sig
    1.12 +  val get: unit -> (string * string) list
    1.13 +  val setmp: (string * string) list -> ('a -> 'b) -> 'a -> 'b
    1.14 +end;
    1.15 +
    1.16 +structure Thread_Position: THREAD_POSITION =
    1.17 +struct
    1.18 +
    1.19 +val var = Thread_Data.var () : (string * string) list Thread_Data.var;
    1.20 +
    1.21 +fun get () =
    1.22 +  (case Thread_Data.get var of
    1.23 +    NONE => []
    1.24 +  | SOME props => props);
    1.25 +
    1.26 +fun setmp props f x =
    1.27 +  Thread_Data.setmp var (if List.null props then NONE else SOME props) f x;
    1.28 +
    1.29 +end;
     2.1 --- a/src/Pure/General/position.ML	Sat Apr 09 14:40:00 2016 +0200
     2.2 +++ b/src/Pure/General/position.ML	Sat Apr 09 14:52:10 2016 +0200
     2.3 @@ -243,9 +243,8 @@
     2.4  
     2.5  (* thread data *)
     2.6  
     2.7 -val thread_data_var = Thread_Data.var () : T Thread_Data.var;
     2.8 -fun thread_data () = the_default none (Thread_Data.get thread_data_var);
     2.9 -fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
    2.10 +val thread_data = of_properties o Thread_Position.get;
    2.11 +fun setmp_thread_data pos = Thread_Position.setmp (properties_of pos);
    2.12  
    2.13  fun default pos =
    2.14    if pos = none then (false, thread_data ())
     3.1 --- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:40:00 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:52:10 2016 +0200
     3.3 @@ -65,9 +65,10 @@
     3.4        "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
     3.5    val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
     3.6    val bootstrap_structures =
     3.7 -    ["Exn", "Basic_Exn", "Thread_Data", "ML_Recursive", "PolyML"] @ hidden_structures;
     3.8 +    ["Exn", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive", "PolyML"] @
     3.9 +      hidden_structures;
    3.10    val bootstrap_signatures =
    3.11 -    ["EXN", "BASIC_EXN", "THREAD_DATA", "ML_RECURSIVE"];
    3.12 +    ["EXN", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE"];
    3.13  
    3.14  
    3.15    (* Standard ML environment *)
     4.1 --- a/src/Pure/ROOT0.ML	Sat Apr 09 14:40:00 2016 +0200
     4.2 +++ b/src/Pure/ROOT0.ML	Sat Apr 09 14:52:10 2016 +0200
     4.3 @@ -4,5 +4,6 @@
     4.4  
     4.5  ML_file "Concurrent/thread_attributes.ML";
     4.6  ML_file "Concurrent/thread_data.ML";
     4.7 +ML_file "Concurrent/thread_position.ML";
     4.8  
     4.9  ML_file "ML/ml_recursive.ML";