author | wenzelm |
Fri, 01 Apr 2016 17:41:41 +0200 | |
changeset 62798 | 2948681ea85f |
parent 62797 | e08c44eed27f |
child 62800 | 7ac100f86863 |
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 |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
10 |
val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
11 |
val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T} |
23673 | 12 |
val line_of: T -> int option |
27795 | 13 |
val offset_of: T -> int option |
41484 | 14 |
val end_offset_of: T -> int option |
23673 | 15 |
val file_of: T -> string option |
27796 | 16 |
val advance: Symbol.symbol -> T -> T |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
17 |
val advance_offset: int -> T -> T |
27796 | 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 |
44200 | 22 |
val file_only: string -> T |
27777 | 23 |
val file: string -> T |
56437 | 24 |
val line_file_only: int -> string -> T |
25 |
val line_file: int -> string -> T |
|
5010 | 26 |
val line: int -> T |
29307 | 27 |
val id: string -> T |
32573 | 28 |
val id_only: string -> T |
27426 | 29 |
val get_id: T -> string option |
30 |
val put_id: string -> T -> T |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset
|
31 |
val parse_id: T -> int option |
28017 | 32 |
val of_properties: Properties.T -> T |
33 |
val properties_of: T -> Properties.T |
|
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42204
diff
changeset
|
34 |
val def_properties_of: T -> Properties.T |
45412 | 35 |
val entity_properties_of: bool -> serial -> T -> Properties.T |
28017 | 36 |
val default_properties: T -> Properties.T -> Properties.T |
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
37 |
val markup: T -> Markup.T -> Markup.T |
41504 | 38 |
val is_reported: T -> bool |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56437
diff
changeset
|
39 |
val is_reported_range: T -> bool |
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
40 |
val reported_text: T -> Markup.T -> string -> string |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
41 |
val report_text: T -> Markup.T -> string -> unit |
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset
|
42 |
val report: T -> Markup.T -> unit |
44736 | 43 |
type report = T * Markup.T |
48767 | 44 |
type report_text = report * string |
45 |
val reports_text: report_text list -> unit |
|
44736 | 46 |
val reports: report list -> unit |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
47 |
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
|
48 |
T list -> ('a -> Markup.T list) -> 'a -> unit |
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
49 |
val append_reports: report_text list Unsynchronized.ref -> report list -> unit |
48992 | 50 |
val here: T -> string |
49691 | 51 |
val here_list: T list -> string |
27764 | 52 |
type range = T * T |
27796 | 53 |
val no_range: range |
62798 | 54 |
val reset_range: T -> T |
62797 | 55 |
val range_position: range -> T |
56 |
val range: T * T -> range |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
57 |
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
|
58 |
val properties_of_range: range -> Properties.T |
25817 | 59 |
val thread_data: unit -> T |
60 |
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
|
61 |
val default: T -> bool * T |
5010 | 62 |
end; |
63 |
||
64 |
structure Position: POSITION = |
|
65 |
struct |
|
66 |
||
67 |
(* datatype position *) |
|
68 |
||
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
69 |
datatype T = Pos of (int * int * int) * Properties.T; |
41484 | 70 |
|
71 |
fun norm_props (props: Properties.T) = |
|
45666 | 72 |
maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
73 |
Markup.position_properties'; |
41484 | 74 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
75 |
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
76 |
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props}; |
27777 | 77 |
|
27795 | 78 |
fun valid (i: int) = i > 0; |
79 |
fun if_valid i i' = if valid i then i' else i; |
|
80 |
||
27777 | 81 |
|
27796 | 82 |
(* fields *) |
83 |
||
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
84 |
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE; |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
85 |
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE; |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
86 |
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE; |
27796 | 87 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
88 |
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; |
27796 | 89 |
|
90 |
||
27777 | 91 |
(* advance *) |
26003 | 92 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
93 |
fun advance_count "\n" (i: int, j: int, k: int) = |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
94 |
(if_valid i (i + 1), if_valid j (j + 1), k) |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
95 |
| advance_count s (i, j, k) = |
58854 | 96 |
if Symbol.not_eof s then (i, if_valid j (j + 1), k) |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
97 |
else (i, j, k); |
5010 | 98 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
99 |
fun invalid_count (i, j, _: int) = |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
100 |
not (valid i orelse valid j); |
27795 | 101 |
|
102 |
fun advance sym (pos as (Pos (count, props))) = |
|
103 |
if invalid_count count then pos else Pos (advance_count sym count, props); |
|
27777 | 104 |
|
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
105 |
fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) = |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
106 |
if invalid_count count then pos |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
107 |
else if valid i then raise Fail "Illegal line position" |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
108 |
else Pos ((i, if_valid j (j + offset), k), props); |
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset
|
109 |
|
27777 | 110 |
|
27796 | 111 |
(* distance of adjacent positions *) |
27777 | 112 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
113 |
fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) = |
27796 | 114 |
if valid j andalso valid j' then j' - j |
115 |
else 0; |
|
26882 | 116 |
|
5010 | 117 |
|
27777 | 118 |
(* make position *) |
119 |
||
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
120 |
val none = Pos ((0, 0, 0), []); |
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
121 |
val start = Pos ((1, 1, 0), []); |
27744 | 122 |
|
29307 | 123 |
|
27796 | 124 |
fun file_name "" = [] |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
125 |
| file_name name = [(Markup.fileN, name)]; |
27796 | 126 |
|
44200 | 127 |
fun file_only name = Pos ((0, 0, 0), file_name name); |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
128 |
fun file name = Pos ((1, 1, 0), file_name name); |
27744 | 129 |
|
56437 | 130 |
fun line_file_only i name = Pos ((i, 0, 0), file_name name); |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
131 |
fun line_file i name = Pos ((i, 1, 0), file_name name); |
27795 | 132 |
fun line i = line_file i ""; |
5010 | 133 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
134 |
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]); |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
135 |
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); |
22158 | 136 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
137 |
fun get_id (Pos (_, props)) = Properties.get props Markup.idN; |
62750 | 138 |
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props)); |
27426 | 139 |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset
|
140 |
fun parse_id pos = Option.map Markup.parse_int (get_id pos); |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset
|
141 |
|
29307 | 142 |
|
143 |
(* markup properties *) |
|
144 |
||
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
145 |
fun get props name = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
146 |
(case Properties.get props name of |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
147 |
NONE => 0 |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
148 |
| SOME s => Markup.parse_int s); |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
149 |
|
25817 | 150 |
fun of_properties props = |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
151 |
make {line = get props Markup.lineN, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
152 |
offset = get props Markup.offsetN, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
153 |
end_offset = get props Markup.end_offsetN, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
154 |
props = props}; |
26003 | 155 |
|
50254
935ac0ad7e83
prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents:
50201
diff
changeset
|
156 |
fun value k i = if valid i then [(k, Markup.print_int i)] else []; |
41484 | 157 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset
|
158 |
fun properties_of (Pos ((i, j, k), props)) = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
159 |
value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props; |
26003 | 160 |
|
54038 | 161 |
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); |
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42204
diff
changeset
|
162 |
|
57899
5867d1306712
clarified signature: entity serial number is not position id;
wenzelm
parents:
56532
diff
changeset
|
163 |
fun entity_properties_of def serial pos = |
5867d1306712
clarified signature: entity serial number is not position id;
wenzelm
parents:
56532
diff
changeset
|
164 |
if def then (Markup.defN, Markup.print_int serial) :: properties_of pos |
5867d1306712
clarified signature: entity serial number is not position id;
wenzelm
parents:
56532
diff
changeset
|
165 |
else (Markup.refN, Markup.print_int serial) :: def_properties_of pos; |
45412 | 166 |
|
26052 | 167 |
fun default_properties default props = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset
|
168 |
if exists (member (op =) Markup.position_properties o #1) props then props |
26052 | 169 |
else properties_of default @ props; |
170 |
||
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
171 |
val markup = Markup.properties o properties_of; |
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
172 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
173 |
|
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset
|
174 |
(* 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
|
175 |
|
41504 | 176 |
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos); |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56437
diff
changeset
|
177 |
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
|
178 |
|
41504 | 179 |
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
|
180 |
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
|
181 |
fun report pos markup = report_text pos markup ""; |
27764 | 182 |
|
44736 | 183 |
type report = T * Markup.T; |
48767 | 184 |
type report_text = report * string; |
44736 | 185 |
|
48767 | 186 |
val reports_text = |
187 |
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
|
188 |
#> Output.report; |
42204 | 189 |
|
48767 | 190 |
val reports = map (rpair "") #> reports_text; |
191 |
||
44735 | 192 |
fun store_reports _ [] _ _ = () |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
193 |
| store_reports (r: report_text list Unsynchronized.ref) ps markup x = |
42204 | 194 |
let val ms = markup x |
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset
|
195 |
in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; |
42204 | 196 |
|
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
197 |
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
|
198 |
Unsynchronized.change r (append (map (rpair "") reports)); |
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset
|
199 |
|
25817 | 200 |
|
56532
3da244bc02bd
tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents:
56459
diff
changeset
|
201 |
(* here: user output *) |
26003 | 202 |
|
48992 | 203 |
fun here pos = |
26003 | 204 |
let |
205 |
val props = properties_of pos; |
|
55624 | 206 |
val (s1, s2) = |
26003 | 207 |
(case (line_of pos, file_of pos) of |
55624 | 208 |
(SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")") |
209 |
| (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")") |
|
210 |
| (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") |
|
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
59085
diff
changeset
|
211 |
| _ => if is_reported pos then ("", "\<here>") else ("", "")); |
26003 | 212 |
in |
213 |
if null props then "" |
|
55624 | 214 |
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 |
26003 | 215 |
end; |
25817 | 216 |
|
49691 | 217 |
val here_list = space_implode " " o map here; |
218 |
||
23627 | 219 |
|
27736 | 220 |
(* range *) |
221 |
||
222 |
type range = T * T; |
|
223 |
||
27796 | 224 |
val no_range = (none, none); |
225 |
||
62798 | 226 |
fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); |
62797 | 227 |
fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); |
62798 | 228 |
fun range (pos, pos') = (range_position (pos, pos'), reset_range pos'); |
27777 | 229 |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
230 |
fun range_of_properties props = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
231 |
let |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
232 |
val pos = of_properties props; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
233 |
val pos' = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
234 |
make {line = get props Markup.end_lineN, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
235 |
offset = get props Markup.end_offsetN, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
236 |
end_offset = 0, |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
237 |
props = props}; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
238 |
in (pos, pos') end; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
239 |
|
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
240 |
fun properties_of_range (pos, pos') = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
241 |
properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos')); |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset
|
242 |
|
27764 | 243 |
|
244 |
(* thread data *) |
|
245 |
||
246 |
local val tag = Universal.tag () : T Universal.tag in |
|
27741 | 247 |
|
28122 | 248 |
fun thread_data () = the_default none (Thread.getLocal tag); |
27764 | 249 |
|
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
|
250 |
fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos; |
27764 | 251 |
|
5010 | 252 |
end; |
27764 | 253 |
|
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
254 |
fun default pos = |
49528
789b73fcca72
report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents:
48992
diff
changeset
|
255 |
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
|
256 |
else (true, pos); |
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset
|
257 |
|
27764 | 258 |
end; |