62929
|
1 |
(* Title: Pure/Concurrent/thread_position.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Thread-local position information.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature THREAD_POSITION =
|
|
8 |
sig
|
62940
|
9 |
type T = {line: int, offset: int, end_offset: int, props: (string * string) list}
|
|
10 |
val none: T
|
|
11 |
val get: unit -> T
|
|
12 |
val setmp: T -> ('a -> 'b) -> 'a -> 'b
|
62929
|
13 |
end;
|
|
14 |
|
|
15 |
structure Thread_Position: THREAD_POSITION =
|
|
16 |
struct
|
|
17 |
|
62940
|
18 |
type T = {line: int, offset: int, end_offset: int, props: (string * string) list};
|
|
19 |
|
|
20 |
val var = Thread_Data.var () : T Thread_Data.var;
|
62929
|
21 |
|
62940
|
22 |
val none: T = {line = 0, offset = 0, end_offset = 0, props = []};
|
62929
|
23 |
|
62940
|
24 |
fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
|
|
25 |
fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
|
62929
|
26 |
|
|
27 |
end;
|