author | wenzelm |
Sat, 01 Apr 2023 14:32:02 +0200 | |
changeset 77770 | 472e48ed9c79 |
parent 77769 | 17391f298cf5 |
child 77771 | 279b18bb4059 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/position.ML |
74165 | 2 |
Author: Makarius |
5010 | 3 |
|
74165 | 4 |
Source positions starting from 1; values <= 0 mean "absent". Count Isabelle |
5 |
symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a |
|
6 |
right-open interval offset .. end_offset (exclusive). |
|
5010 | 7 |
*) |
8 |
||
9 |
signature POSITION = |
|
10 |
sig |
|
41484 | 11 |
eqtype T |
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
12 |
val ord: T ord |
62940 | 13 |
val make: Thread_Position.T -> T |
14 |
val dest: T -> Thread_Position.T |
|
23673 | 15 |
val line_of: T -> int option |
27795 | 16 |
val offset_of: T -> int option |
41484 | 17 |
val end_offset_of: T -> int option |
23673 | 18 |
val file_of: T -> string option |
74166 | 19 |
val id_of: T -> string option |
74174 | 20 |
val symbol: Symbol.symbol -> T -> T |
21 |
val symbol_explode: string -> T -> T |
|
68177 | 22 |
val distance_of: T * T -> int option |
5010 | 23 |
val none: T |
27777 | 24 |
val start: T |
31435 | 25 |
val file_name: string -> Properties.T |
44200 | 26 |
val file_only: string -> T |
27777 | 27 |
val file: string -> T |
56437 | 28 |
val line_file_only: int -> string -> T |
29 |
val line_file: int -> string -> T |
|
5010 | 30 |
val line: int -> T |
67280
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
64556
diff
changeset
|
31 |
val get_props: T -> Properties.T |
29307 | 32 |
val id: string -> T |
32573 | 33 |
val id_only: string -> T |
27426 | 34 |
val put_id: string -> T -> T |
68858 | 35 |
val copy_id: T -> T -> T |
68829 | 36 |
val id_properties_of: T -> Properties.T |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset
|
37 |
val parse_id: T -> int option |
74180 | 38 |
val advance_offsets: int -> T -> T |
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
39 |
val adjust_offsets: (int -> int option) -> T -> T |
28017 | 40 |
val of_properties: Properties.T -> T |
41 |
val properties_of: T -> Properties.T |
|
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42204
diff
changeset
|
42 |
val def_properties_of: T -> Properties.T |
71910 | 43 |
val entity_markup: string -> string * T -> Markup.T |
74262 | 44 |
val make_entity_markup: {def: bool} -> serial -> string -> string * T -> Markup.T |
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
45 |
val markup: T -> Markup.T -> Markup.T |
41504 | 46 |
val is_reported: T -> bool |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56437
diff
changeset
|
47 |
val is_reported_range: T -> bool |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
48 |
val reported_text: T -> Markup.T -> string -> string |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
49 |
val report_text: T -> Markup.T -> string -> unit |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
50 |
val report: T -> Markup.T -> unit |
44736 | 51 |
type report = T * Markup.T |
48767 | 52 |
type report_text = report * string |
53 |
val reports_text: report_text list -> unit |
|
44736 | 54 |
val reports: report list -> unit |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
55 |
val store_reports: report_text list Unsynchronized.ref -> |
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
56 |
T list -> ('a -> Markup.T list) -> 'a -> unit |
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
57 |
val append_reports: report_text list Unsynchronized.ref -> report list -> unit |
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
58 |
val here_strs: T -> string * string |
48992 | 59 |
val here: T -> string |
49691 | 60 |
val here_list: T list -> string |
27764 | 61 |
type range = T * T |
27796 | 62 |
val no_range: range |
62800 | 63 |
val no_range_position: T -> T |
62797 | 64 |
val range_position: range -> T |
65 |
val range: T * T -> range |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
66 |
val range_of_properties: Properties.T -> range |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
67 |
val properties_of_range: range -> Properties.T |
25817 | 68 |
val thread_data: unit -> T |
69 |
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b |
|
49528
789b73fcca72
report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents:
48992
diff
changeset
|
70 |
val default: T -> bool * T |
5010 | 71 |
end; |
72 |
||
73 |
structure Position: POSITION = |
|
74 |
struct |
|
75 |
||
76 |
(* datatype position *) |
|
77 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
78 |
datatype T = Pos of {line: int, offset: int, end_offset: int, props: Properties.T}; |
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
79 |
|
41484 | 80 |
fun norm_props (props: Properties.T) = |
45666 | 81 |
maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) |
72707 | 82 |
[Markup.fileN, Markup.idN]; |
41484 | 83 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
84 |
fun make {line, offset, end_offset, props} = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
85 |
Pos {line = line, offset = offset, end_offset = end_offset, props = norm_props props}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
86 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
87 |
fun dest (Pos args) = args; |
27777 | 88 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
89 |
val ord = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
90 |
pointer_eq_ord |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
91 |
(int_ord o apply2 (#line o dest) ||| |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
92 |
int_ord o apply2 (#offset o dest) ||| |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
93 |
int_ord o apply2 (#end_offset o dest) ||| |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
94 |
Properties.ord o apply2 (#props o dest)); |
27795 | 95 |
|
27777 | 96 |
|
27796 | 97 |
(* fields *) |
98 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
99 |
fun valid (i: int) = i > 0; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
100 |
fun maybe_valid i = if valid i then SOME i else NONE; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
101 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
102 |
val invalid = not o valid; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
103 |
fun invalid_pos (Pos {line, offset, ...}) = invalid line andalso invalid offset; |
27796 | 104 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
105 |
val line_of = maybe_valid o #line o dest; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
106 |
val offset_of = maybe_valid o #offset o dest; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
107 |
val end_offset_of = maybe_valid o #end_offset o dest; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
108 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
109 |
fun file_of (Pos {props, ...}) = Properties.get props Markup.fileN; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
110 |
fun id_of (Pos {props, ...}) = Properties.get props Markup.idN; |
27796 | 111 |
|
112 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
113 |
(* symbol positions *) |
5010 | 114 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
115 |
fun symbols [] pos = pos |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
116 |
| symbols ss (pos as Pos {line, offset, end_offset, props}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
117 |
let |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
118 |
val line' = if valid line then fold (fn s => s = "\n" ? Integer.add 1) ss line else line; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
119 |
val offset' = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
120 |
if valid offset then fold (fn s => Symbol.not_eof s ? Integer.add 1) ss offset else offset; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
121 |
in |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
122 |
if line = line' andalso offset = offset' then pos |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
123 |
else Pos {line = line', offset = offset', end_offset = end_offset, props = props} |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
124 |
end; |
27795 | 125 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
126 |
val symbol = symbols o single; |
27777 | 127 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
128 |
fun symbol_explode str pos = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
129 |
if str = "" orelse invalid_pos pos then pos |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
130 |
else fold symbol (Symbol.explode str) pos; |
74171 | 131 |
|
74176 | 132 |
|
27796 | 133 |
(* distance of adjacent positions *) |
27777 | 134 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
135 |
fun distance_of (Pos {offset, ...}, Pos {offset = offset', ...}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
136 |
if valid offset andalso valid offset' then SOME (offset' - offset) else NONE; |
26882 | 137 |
|
5010 | 138 |
|
27777 | 139 |
(* make position *) |
140 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
141 |
val none = Pos {line = 0, offset = 0, end_offset = 0, props = []}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
142 |
val start = Pos {line = 1, offset = 1, end_offset = 0, props = []}; |
27744 | 143 |
|
29307 | 144 |
|
27796 | 145 |
fun file_name "" = [] |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
146 |
| file_name name = [(Markup.fileN, name)]; |
27796 | 147 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
148 |
fun file_only name = Pos {line = 0, offset = 0, end_offset = 0, props = file_name name}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
149 |
fun file name = Pos {line = 1, offset = 1, end_offset = 0, props = file_name name}; |
27744 | 150 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
151 |
fun line_file_only line name = Pos {line = line, offset = 0, end_offset = 0, props = file_name name}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
152 |
fun line_file line name = Pos {line = line, offset = 1, end_offset = 0, props = file_name name}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
153 |
fun line line = line_file line ""; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
154 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
155 |
val get_props = #props o dest; |
5010 | 156 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
157 |
fun id id = Pos {line = 0, offset = 1, end_offset = 0, props = [(Markup.idN, id)]}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
158 |
fun id_only id = Pos {line = 0, offset = 0, end_offset = 0, props = [(Markup.idN, id)]}; |
67280
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
64556
diff
changeset
|
159 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
160 |
fun put_id id (pos as Pos {line, offset, end_offset, props}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
161 |
let val props' = norm_props (Properties.put (Markup.idN, id) props) in |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
162 |
if props = props' then pos |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
163 |
else Pos {line = line, offset = offset, end_offset = end_offset, props = props'} |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
164 |
end; |
22158 | 165 |
|
74166 | 166 |
fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id); |
27426 | 167 |
|
74166 | 168 |
fun parse_id pos = Option.map Value.parse_int (id_of pos); |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset
|
169 |
|
68829 | 170 |
fun id_properties_of pos = |
74166 | 171 |
(case id_of pos of |
68829 | 172 |
SOME id => [(Markup.idN, id)] |
173 |
| NONE => []); |
|
29307 | 174 |
|
74180 | 175 |
|
176 |
(* adjust offsets *) |
|
177 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
178 |
fun shift_offsets {remove_id} shift (pos as Pos {line, offset, end_offset, props}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
179 |
if shift < 0 then raise Fail "Illegal offset shift" |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
180 |
else if shift > 0 andalso valid line then raise Fail "Illegal line position" |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
181 |
else |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
182 |
let |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
183 |
val offset' = if valid offset then offset + shift else offset; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
184 |
val end_offset' = if valid end_offset then end_offset + shift else end_offset; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
185 |
val props' = if remove_id then Properties.remove Markup.idN props else props; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
186 |
in |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
187 |
if offset = offset' andalso end_offset = end_offset' andalso props = props' then pos |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
188 |
else Pos {line = line, offset = offset', end_offset = end_offset', props = props'} |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
189 |
end; |
74180 | 190 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
191 |
val advance_offsets = shift_offsets {remove_id = false}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
192 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
193 |
fun adjust_offsets adjust pos = |
68858 | 194 |
if is_none (file_of pos) then |
195 |
(case parse_id pos of |
|
196 |
SOME id => |
|
197 |
(case adjust id of |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
198 |
SOME shift => shift_offsets {remove_id = true} shift pos |
68858 | 199 |
| NONE => pos) |
200 |
| NONE => pos) |
|
201 |
else pos; |
|
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
202 |
|
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
203 |
|
29307 | 204 |
(* markup properties *) |
205 |
||
74181 | 206 |
fun get_int props name = |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
207 |
(case Properties.get props name of |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
208 |
NONE => 0 |
63806 | 209 |
| SOME s => Value.parse_int s); |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
210 |
|
25817 | 211 |
fun of_properties props = |
74181 | 212 |
make { |
213 |
line = get_int props Markup.lineN, |
|
214 |
offset = get_int props Markup.offsetN, |
|
215 |
end_offset = get_int props Markup.end_offsetN, |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
216 |
props = props}; |
26003 | 217 |
|
74181 | 218 |
fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)]; |
41484 | 219 |
|
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
220 |
fun properties_of (Pos {line, offset, end_offset, props}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
221 |
int_entry Markup.lineN line @ |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
222 |
int_entry Markup.offsetN offset @ |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
223 |
int_entry Markup.end_offsetN end_offset @ props; |
26003 | 224 |
|
74182 | 225 |
val def_properties_of = properties_of #> map (apfst Markup.def_name); |
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42204
diff
changeset
|
226 |
|
71910 | 227 |
fun entity_markup kind (name, pos) = |
228 |
Markup.entity kind name |> Markup.properties (def_properties_of pos); |
|
229 |
||
74262 | 230 |
fun make_entity_markup {def} serial kind (name, pos) = |
74183 | 231 |
let |
232 |
val props = |
|
233 |
if def then (Markup.defN, Value.print_int serial) :: properties_of pos |
|
234 |
else (Markup.refN, Value.print_int serial) :: def_properties_of pos; |
|
235 |
in Markup.entity kind name |> Markup.properties props end; |
|
45412 | 236 |
|
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
237 |
val markup = Markup.properties o properties_of; |
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
238 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
239 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
240 |
(* 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
|
241 |
|
74166 | 242 |
fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos); |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56437
diff
changeset
|
243 |
fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos); |
30669
6de7ef888aa3
added report_text -- status messages with text body;
wenzelm
parents:
29307
diff
changeset
|
244 |
|
41504 | 245 |
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else ""; |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
55959
diff
changeset
|
246 |
fun report_text pos markup txt = Output.report [reported_text pos markup txt]; |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
247 |
fun report pos markup = report_text pos markup ""; |
27764 | 248 |
|
44736 | 249 |
type report = T * Markup.T; |
48767 | 250 |
type report_text = report * string; |
44736 | 251 |
|
48767 | 252 |
val reports_text = |
253 |
map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "") |
|
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
55959
diff
changeset
|
254 |
#> Output.report; |
42204 | 255 |
|
48767 | 256 |
val reports = map (rpair "") #> reports_text; |
257 |
||
44735 | 258 |
fun store_reports _ [] _ _ = () |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
259 |
| store_reports (r: report_text list Unsynchronized.ref) ps markup x = |
42204 | 260 |
let val ms = markup x |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
261 |
in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; |
42204 | 262 |
|
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
263 |
fun append_reports (r: report_text list Unsynchronized.ref) reports = |
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
264 |
Unsynchronized.change r (append (map (rpair "") reports)); |
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
265 |
|
25817 | 266 |
|
56532
3da244bc02bd
tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents:
56459
diff
changeset
|
267 |
(* here: user output *) |
26003 | 268 |
|
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
269 |
fun here_strs pos = |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
270 |
(case (line_of pos, file_of pos) of |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
271 |
(SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
272 |
| (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
273 |
| (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
274 |
| _ => if is_reported pos then ("", "\092<^here>") else ("", "")); |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
275 |
|
48992 | 276 |
fun here pos = |
26003 | 277 |
let |
278 |
val props = properties_of pos; |
|
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
70498
diff
changeset
|
279 |
val (s1, s2) = here_strs pos; |
26003 | 280 |
in |
69348 | 281 |
if s2 = "" then "" |
55624 | 282 |
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 |
26003 | 283 |
end; |
25817 | 284 |
|
70498 | 285 |
val here_list = map here #> distinct (op =) #> implode; |
49691 | 286 |
|
23627 | 287 |
|
27736 | 288 |
(* range *) |
289 |
||
290 |
type range = T * T; |
|
291 |
||
27796 | 292 |
val no_range = (none, none); |
293 |
||
77769
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
294 |
fun no_range_position (Pos {line, offset, end_offset = _, props}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
295 |
Pos {line = line, offset = offset, end_offset = 0, props = props}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
296 |
|
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
297 |
fun range_position (Pos {line, offset, end_offset = _, props}, Pos {offset = offset', ...}) = |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
298 |
Pos {line = line, offset = offset, end_offset = offset', props = props}; |
17391f298cf5
misc tuning and clarification: more tight representation;
wenzelm
parents:
74262
diff
changeset
|
299 |
|
62800 | 300 |
fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos'); |
27777 | 301 |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
302 |
fun range_of_properties props = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
303 |
let |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
304 |
val pos = of_properties props; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
305 |
val pos' = |
74181 | 306 |
make {line = get_int props Markup.end_lineN, |
307 |
offset = get_int props Markup.end_offsetN, |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
308 |
end_offset = 0, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
309 |
props = props}; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
310 |
in (pos, pos') end; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
311 |
|
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
312 |
fun properties_of_range (pos, pos') = |
74181 | 313 |
properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos')); |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
314 |
|
27764 | 315 |
|
316 |
(* thread data *) |
|
317 |
||
62940 | 318 |
val thread_data = make o Thread_Position.get; |
319 |
fun setmp_thread_data pos = Thread_Position.setmp (dest pos); |
|
27764 | 320 |
|
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
321 |
fun default pos = |
49528
789b73fcca72
report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents:
48992
diff
changeset
|
322 |
if pos = none then (false, thread_data ()) |
789b73fcca72
report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents:
48992
diff
changeset
|
323 |
else (true, pos); |
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
324 |
|
27764 | 325 |
end; |