author | wenzelm |
Wed, 04 Mar 2009 23:05:32 +0100 | |
changeset 30266 | 970bf4f594c9 |
parent 29307 | 3a0b38b7fbb4 |
child 30669 | 6de7ef888aa3 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/position.ML |
5010 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
29307 | 4 |
Source positions: counting Isabelle symbols, starting from 1. |
5010 | 5 |
*) |
6 |
||
7 |
signature POSITION = |
|
8 |
sig |
|
9 |
type T |
|
23673 | 10 |
val line_of: T -> int option |
26003 | 11 |
val column_of: T -> int option |
27795 | 12 |
val offset_of: T -> int option |
23673 | 13 |
val file_of: T -> string option |
27796 | 14 |
val advance: Symbol.symbol -> T -> T |
15 |
val distance_of: T -> T -> int |
|
5010 | 16 |
val none: T |
27777 | 17 |
val start: T |
18 |
val file: string -> T |
|
5010 | 19 |
val line: int -> T |
27777 | 20 |
val line_file: int -> string -> T |
29307 | 21 |
val id: string -> T |
27426 | 22 |
val get_id: T -> string option |
23 |
val put_id: string -> T -> T |
|
28017 | 24 |
val of_properties: Properties.T -> T |
25 |
val properties_of: T -> Properties.T |
|
26 |
val default_properties: T -> Properties.T -> Properties.T |
|
27764 | 27 |
val report: Markup.T -> T -> unit |
26003 | 28 |
val str_of: T -> string |
27764 | 29 |
type range = T * T |
27796 | 30 |
val no_range: range |
27764 | 31 |
val encode_range: range -> T |
27777 | 32 |
val reset_range: T -> T |
27764 | 33 |
val range: T -> T -> range |
25817 | 34 |
val thread_data: unit -> T |
35 |
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b |
|
25954 | 36 |
val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
5010 | 37 |
end; |
38 |
||
39 |
structure Position: POSITION = |
|
40 |
struct |
|
41 |
||
42 |
(* datatype position *) |
|
43 |
||
28017 | 44 |
datatype T = Pos of (int * int * int) * Properties.T; |
27777 | 45 |
|
27795 | 46 |
fun valid (i: int) = i > 0; |
47 |
fun if_valid i i' = if valid i then i' else i; |
|
48 |
||
49 |
fun value k i = if valid i then [(k, string_of_int i)] else []; |
|
27777 | 50 |
|
51 |
||
27796 | 52 |
(* fields *) |
53 |
||
54 |
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE; |
|
55 |
fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE; |
|
56 |
fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE; |
|
57 |
||
28017 | 58 |
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; |
27796 | 59 |
|
60 |
||
27777 | 61 |
(* advance *) |
26003 | 62 |
|
27795 | 63 |
fun advance_count "\n" (i: int, j: int, k: int) = |
64 |
(if_valid i (i + 1), if_valid j 1, if_valid k (k + 1)) |
|
65 |
| advance_count s (i, j, k) = |
|
66 |
if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s) |
|
67 |
then (i, if_valid j (j + 1), if_valid k (k + 1)) else (i, j, k); |
|
5010 | 68 |
|
27795 | 69 |
fun invalid_count (i, j, k) = |
70 |
not (valid i orelse valid j orelse valid k); |
|
71 |
||
72 |
fun advance sym (pos as (Pos (count, props))) = |
|
73 |
if invalid_count count then pos else Pos (advance_count sym count, props); |
|
27777 | 74 |
|
75 |
||
27796 | 76 |
(* distance of adjacent positions *) |
27777 | 77 |
|
27796 | 78 |
fun distance_of (Pos ((_, j, k), _)) (Pos ((_, j', k'), _)) = |
79 |
if valid j andalso valid j' then j' - j |
|
80 |
else if valid k andalso valid k' then k' - k |
|
81 |
else 0; |
|
26882 | 82 |
|
5010 | 83 |
|
27777 | 84 |
(* make position *) |
85 |
||
27795 | 86 |
val none = Pos ((0, 0, 0), []); |
87 |
val start = Pos ((1, 1, 1), []); |
|
27744 | 88 |
|
29307 | 89 |
|
27796 | 90 |
fun file_name "" = [] |
91 |
| file_name name = [(Markup.fileN, name)]; |
|
92 |
||
27795 | 93 |
fun file name = Pos ((1, 1, 1), file_name name); |
27744 | 94 |
|
27795 | 95 |
fun line_file i name = Pos ((i, 0, 0), file_name name); |
96 |
fun line i = line_file i ""; |
|
5010 | 97 |
|
23627 | 98 |
|
29307 | 99 |
fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]); |
22158 | 100 |
|
28017 | 101 |
fun get_id (Pos (_, props)) = Properties.get props Markup.idN; |
102 |
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props); |
|
27426 | 103 |
|
29307 | 104 |
|
105 |
(* markup properties *) |
|
106 |
||
25817 | 107 |
fun of_properties props = |
23627 | 108 |
let |
27795 | 109 |
fun get name = |
28017 | 110 |
(case Properties.get props name of |
27795 | 111 |
NONE => 0 |
112 |
| SOME s => the_default 0 (Int.fromString s)); |
|
113 |
val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN); |
|
26003 | 114 |
fun property name = the_list (find_first (fn (x: string, _) => x = name) props); |
27749
24f2b57a34ea
of_properties: observe Markup.position_properties';
wenzelm
parents:
27744
diff
changeset
|
115 |
in Pos (count, maps property Markup.position_properties') end; |
26003 | 116 |
|
27795 | 117 |
fun properties_of (Pos ((i, j, k), props)) = |
118 |
value Markup.lineN i @ value Markup.columnN j @ value Markup.offsetN k @ props; |
|
26003 | 119 |
|
26052 | 120 |
fun default_properties default props = |
121 |
if exists (member (op =) Markup.position_properties o #1) props then props |
|
122 |
else properties_of default @ props; |
|
123 |
||
27795 | 124 |
fun report markup (pos as Pos (count, _)) = |
125 |
if invalid_count count then () |
|
27764 | 126 |
else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) ""); |
127 |
||
25817 | 128 |
|
26003 | 129 |
(* str_of *) |
130 |
||
131 |
fun str_of pos = |
|
132 |
let |
|
133 |
val props = properties_of pos; |
|
134 |
val s = |
|
135 |
(case (line_of pos, file_of pos) of |
|
27795 | 136 |
(SOME i, NONE) => "(line " ^ string_of_int i ^ ")" |
137 |
| (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")" |
|
26003 | 138 |
| _ => ""); |
139 |
in |
|
140 |
if null props then "" |
|
141 |
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s |
|
142 |
end; |
|
25817 | 143 |
|
23627 | 144 |
|
27736 | 145 |
(* range *) |
146 |
||
147 |
type range = T * T; |
|
148 |
||
27796 | 149 |
val no_range = (none, none); |
150 |
||
27795 | 151 |
fun encode_range (Pos (count, props), Pos ((i, j, k), _)) = |
28017 | 152 |
let val props' = props |> fold_rev Properties.put |
27795 | 153 |
(value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k) |
154 |
in Pos (count, props') end; |
|
27777 | 155 |
|
156 |
fun reset_range (Pos (count, props)) = |
|
28017 | 157 |
let val props' = props |> fold Properties.remove |
27795 | 158 |
[Markup.end_lineN, Markup.end_columnN, Markup.end_offsetN] |
159 |
in Pos (count, props') end; |
|
27736 | 160 |
|
27764 | 161 |
fun range pos pos' = (encode_range (pos, pos'), pos'); |
27741 | 162 |
|
27764 | 163 |
|
164 |
(* thread data *) |
|
165 |
||
166 |
local val tag = Universal.tag () : T Universal.tag in |
|
27741 | 167 |
|
28122 | 168 |
fun thread_data () = the_default none (Thread.getLocal tag); |
27764 | 169 |
|
170 |
fun setmp_thread_data pos f x = |
|
171 |
if ! Output.debugging then f x |
|
172 |
else Library.setmp_thread_data tag (thread_data ()) pos f x; |
|
173 |
||
174 |
fun setmp_thread_data_seq pos f x = |
|
175 |
setmp_thread_data pos f x |> Seq.wrap (fn pull => setmp_thread_data pos pull ()); |
|
27741 | 176 |
|
5010 | 177 |
end; |
27764 | 178 |
|
179 |
end; |