author | wenzelm |
Sun, 03 Apr 2011 21:59:33 +0200 | |
changeset 42204 | b3277168c1e7 |
parent 41504 | f0f20a5b54df |
child 42327 | 7c7cc7590eb3 |
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 |
|
41484 | 9 |
eqtype T |
10 |
val make: {line: int, column: int, offset: int, end_offset: int, props: Properties.T} -> T |
|
11 |
val dest: T -> {line: int, column: int, offset: int, end_offset: int, props: Properties.T} |
|
23673 | 12 |
val line_of: T -> int option |
26003 | 13 |
val column_of: T -> int option |
27795 | 14 |
val offset_of: T -> int option |
41484 | 15 |
val end_offset_of: T -> int option |
23673 | 16 |
val file_of: T -> string option |
27796 | 17 |
val advance: Symbol.symbol -> T -> T |
18 |
val distance_of: T -> T -> int |
|
5010 | 19 |
val none: T |
27777 | 20 |
val start: T |
31435 | 21 |
val file_name: string -> Properties.T |
27777 | 22 |
val file: string -> T |
5010 | 23 |
val line: int -> T |
27777 | 24 |
val line_file: int -> string -> T |
29307 | 25 |
val id: string -> T |
32573 | 26 |
val id_only: string -> T |
27426 | 27 |
val get_id: T -> string option |
28 |
val put_id: string -> T -> T |
|
28017 | 29 |
val of_properties: Properties.T -> T |
30 |
val properties_of: T -> Properties.T |
|
31 |
val default_properties: T -> Properties.T -> Properties.T |
|
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
32 |
val markup: T -> Markup.T -> Markup.T |
41504 | 33 |
val is_reported: T -> bool |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
34 |
val reported_text: T -> Markup.T -> string -> string |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
35 |
val report_text: T -> Markup.T -> string -> unit |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
36 |
val report: T -> Markup.T -> unit |
42204 | 37 |
type reports = (T * Markup.T) list |
38 |
val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit |
|
26003 | 39 |
val str_of: T -> string |
27764 | 40 |
type range = T * T |
27796 | 41 |
val no_range: range |
41484 | 42 |
val set_range: range -> T |
27777 | 43 |
val reset_range: T -> T |
27764 | 44 |
val range: T -> T -> range |
25817 | 45 |
val thread_data: unit -> T |
46 |
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b |
|
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
47 |
val default: T -> T |
5010 | 48 |
end; |
49 |
||
50 |
structure Position: POSITION = |
|
51 |
struct |
|
52 |
||
53 |
(* datatype position *) |
|
54 |
||
41484 | 55 |
datatype T = Pos of (int * int * int * int) * Properties.T; |
56 |
||
57 |
fun norm_props (props: Properties.T) = |
|
58 |
maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties'; |
|
59 |
||
60 |
fun make {line = i, column = j, offset = k, end_offset = l, props} = |
|
61 |
Pos ((i, j, k, l), norm_props props); |
|
62 |
||
63 |
fun dest (Pos ((i, j, k, l), props)) = |
|
64 |
{line = i, column = j, offset = k, end_offset = l, props = props}; |
|
65 |
||
27777 | 66 |
|
27795 | 67 |
fun valid (i: int) = i > 0; |
68 |
fun if_valid i i' = if valid i then i' else i; |
|
69 |
||
27777 | 70 |
|
27796 | 71 |
(* fields *) |
72 |
||
41484 | 73 |
fun line_of (Pos ((i, _, _, _), _)) = if valid i then SOME i else NONE; |
74 |
fun column_of (Pos ((_, j, _, _), _)) = if valid j then SOME j else NONE; |
|
75 |
fun offset_of (Pos ((_, _, k, _), _)) = if valid k then SOME k else NONE; |
|
76 |
fun end_offset_of (Pos ((_, _, _, l), _)) = if valid l then SOME l else NONE; |
|
27796 | 77 |
|
28017 | 78 |
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; |
27796 | 79 |
|
80 |
||
27777 | 81 |
(* advance *) |
26003 | 82 |
|
41484 | 83 |
fun advance_count "\n" (i: int, j: int, k: int, l: int) = |
84 |
(if_valid i (i + 1), if_valid j 1, if_valid k (k + 1), l) |
|
85 |
| advance_count s (i, j, k, l) = |
|
86 |
if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1), l) |
|
87 |
else (i, j, k, l); |
|
5010 | 88 |
|
41484 | 89 |
fun invalid_count (i, j, k, _: int) = |
27795 | 90 |
not (valid i orelse valid j orelse valid k); |
91 |
||
92 |
fun advance sym (pos as (Pos (count, props))) = |
|
93 |
if invalid_count count then pos else Pos (advance_count sym count, props); |
|
27777 | 94 |
|
95 |
||
27796 | 96 |
(* distance of adjacent positions *) |
27777 | 97 |
|
41484 | 98 |
fun distance_of (Pos ((_, j, k, _), _)) (Pos ((_, j', k', _), _)) = |
27796 | 99 |
if valid j andalso valid j' then j' - j |
100 |
else if valid k andalso valid k' then k' - k |
|
101 |
else 0; |
|
26882 | 102 |
|
5010 | 103 |
|
27777 | 104 |
(* make position *) |
105 |
||
41484 | 106 |
val none = Pos ((0, 0, 0, 0), []); |
107 |
val start = Pos ((1, 1, 1, 0), []); |
|
27744 | 108 |
|
29307 | 109 |
|
27796 | 110 |
fun file_name "" = [] |
111 |
| file_name name = [(Markup.fileN, name)]; |
|
112 |
||
41484 | 113 |
fun file name = Pos ((1, 1, 1, 0), file_name name); |
27744 | 114 |
|
41484 | 115 |
fun line_file i name = Pos ((i, 0, 0, 0), file_name name); |
27795 | 116 |
fun line i = line_file i ""; |
5010 | 117 |
|
41484 | 118 |
fun id id = Pos ((0, 0, 1, 0), [(Markup.idN, id)]); |
119 |
fun id_only id = Pos ((0, 0, 0, 0), [(Markup.idN, id)]); |
|
22158 | 120 |
|
28017 | 121 |
fun get_id (Pos (_, props)) = Properties.get props Markup.idN; |
122 |
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props); |
|
27426 | 123 |
|
29307 | 124 |
|
125 |
(* markup properties *) |
|
126 |
||
25817 | 127 |
fun of_properties props = |
23627 | 128 |
let |
27795 | 129 |
fun get name = |
28017 | 130 |
(case Properties.get props name of |
27795 | 131 |
NONE => 0 |
132 |
| SOME s => the_default 0 (Int.fromString s)); |
|
41484 | 133 |
in |
134 |
make {line = get Markup.lineN, column = get Markup.columnN, |
|
135 |
offset = get Markup.offsetN, end_offset = get Markup.end_offsetN, props = props} |
|
136 |
end; |
|
137 |
||
26003 | 138 |
|
41484 | 139 |
fun value k i = if valid i then [(k, string_of_int i)] else []; |
140 |
||
141 |
fun properties_of (Pos ((i, j, k, l), props)) = |
|
142 |
value Markup.lineN i @ value Markup.columnN j @ |
|
143 |
value Markup.offsetN k @ value Markup.end_offsetN l @ props; |
|
26003 | 144 |
|
26052 | 145 |
fun default_properties default props = |
146 |
if exists (member (op =) Markup.position_properties o #1) props then props |
|
147 |
else properties_of default @ props; |
|
148 |
||
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
149 |
val markup = Markup.properties o properties_of; |
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
150 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
151 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
152 |
(* reports *) |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38236
diff
changeset
|
153 |
|
41504 | 154 |
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos); |
30669
6de7ef888aa3
added report_text -- status messages with text body;
wenzelm
parents:
29307
diff
changeset
|
155 |
|
41504 | 156 |
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else ""; |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
157 |
fun report_text pos markup txt = Output.report (reported_text pos markup txt); |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
158 |
fun report pos markup = report_text pos markup ""; |
27764 | 159 |
|
42204 | 160 |
type reports = (T * Markup.T) list; |
161 |
||
162 |
fun reports _ [] _ _ = () |
|
163 |
| reports (r: reports Unsynchronized.ref) ps markup x = |
|
164 |
let val ms = markup x |
|
165 |
in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end; |
|
166 |
||
25817 | 167 |
|
26003 | 168 |
(* str_of *) |
169 |
||
170 |
fun str_of pos = |
|
171 |
let |
|
172 |
val props = properties_of pos; |
|
173 |
val s = |
|
174 |
(case (line_of pos, file_of pos) of |
|
27795 | 175 |
(SOME i, NONE) => "(line " ^ string_of_int i ^ ")" |
176 |
| (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")" |
|
26003 | 177 |
| _ => ""); |
178 |
in |
|
179 |
if null props then "" |
|
180 |
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s |
|
181 |
end; |
|
25817 | 182 |
|
23627 | 183 |
|
27736 | 184 |
(* range *) |
185 |
||
186 |
type range = T * T; |
|
187 |
||
27796 | 188 |
val no_range = (none, none); |
189 |
||
41484 | 190 |
fun set_range (Pos ((i, j, k, _), props), Pos ((_, _, k', _), _)) = Pos ((i, j, k, k'), props); |
191 |
fun reset_range (Pos ((i, j, k, _), props)) = Pos ((i, j, k, 0), props); |
|
27777 | 192 |
|
41484 | 193 |
fun range pos pos' = (set_range (pos, pos'), pos'); |
27741 | 194 |
|
27764 | 195 |
|
196 |
(* thread data *) |
|
197 |
||
198 |
local val tag = Universal.tag () : T Universal.tag in |
|
27741 | 199 |
|
28122 | 200 |
fun thread_data () = the_default none (Thread.getLocal tag); |
27764 | 201 |
|
37043
f8e24980af05
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
wenzelm
parents:
33097
diff
changeset
|
202 |
fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos; |
27764 | 203 |
|
5010 | 204 |
end; |
27764 | 205 |
|
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
206 |
fun default pos = |
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
207 |
if pos = none then thread_data () |
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
208 |
else pos; |
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
209 |
|
27764 | 210 |
end; |