src/Pure/Concurrent/thread_position.ML
author wenzelm
Sun, 10 Apr 2016 17:52:30 +0200
changeset 62940 a03592aafadf
parent 62929 b92565f98206
permissions -rw-r--r--
tuned -- avoid recoding properties;
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
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
     9
  type T = {line: int, offset: int, end_offset: int, props: (string * string) list}
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    10
  val none: T
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    11
  val get: unit -> T
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    12
  val setmp: T -> ('a -> 'b) -> 'a -> 'b
62929
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    13
end;
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    14
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    15
structure Thread_Position: THREAD_POSITION =
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    16
struct
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    17
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    18
type T = {line: int, offset: int, end_offset: int, props: (string * string) list};
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    19
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    20
val var = Thread_Data.var () : T Thread_Data.var;
62929
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    21
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    22
val none: T = {line = 0, offset = 0, end_offset = 0, props = []};
62929
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    23
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    24
fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    25
fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
62929
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    26
b92565f98206 shared thread position for physical/virtual Pure;
wenzelm
parents:
diff changeset
    27
end;