author  wenzelm 
Tue, 27 Nov 2018 16:22:12 +0100  
changeset 69348  f0aef5e337a2 
parent 68858  e1796b8ddbae 
child 70498  de75eea6ffc8 
permissions  rwrr 
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 
62940  10 
val make: Thread_Position.T > T 
11 
val dest: T > Thread_Position.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 
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

17 
val advance_offsets: int > T > T 
68177  18 
val distance_of: T * T > int option 
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 
67280
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
64556
diff
changeset

27 
val get_props: T > Properties.T 
29307  28 
val id: string > T 
32573  29 
val id_only: string > T 
27426  30 
val get_id: T > string option 
31 
val put_id: string > T > T 

68858  32 
val copy_id: T > T > T 
68829  33 
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

34 
val parse_id: T > int option 
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

35 
val adjust_offsets: (int > int option) > T > T 
28017  36 
val of_properties: Properties.T > T 
37 
val properties_of: T > Properties.T 

68172  38 
val offset_properties_of: T > Properties.T 
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42204
diff
changeset

39 
val def_properties_of: T > Properties.T 
45412  40 
val entity_properties_of: bool > serial > T > Properties.T 
28017  41 
val default_properties: T > Properties.T > Properties.T 
39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset

42 
val markup: T > Markup.T > Markup.T 
41504  43 
val is_reported: T > bool 
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56437
diff
changeset

44 
val is_reported_range: T > bool 
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

45 
val reported_text: T > Markup.T > string > string 
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

46 
val report_text: T > Markup.T > string > unit 
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39440
diff
changeset

47 
val report: T > Markup.T > unit 
44736  48 
type report = T * Markup.T 
48767  49 
type report_text = report * string 
50 
val reports_text: report_text list > unit 

44736  51 
val reports: report list > unit 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset

52 
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

53 
T list > ('a > Markup.T list) > 'a > unit 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset

54 
val append_reports: report_text list Unsynchronized.ref > report list > unit 
48992  55 
val here: T > string 
49691  56 
val here_list: T list > string 
27764  57 
type range = T * T 
27796  58 
val no_range: range 
62800  59 
val no_range_position: T > T 
62797  60 
val range_position: range > T 
61 
val range: T * T > range 

58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

62 
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

63 
val properties_of_range: range > Properties.T 
25817  64 
val thread_data: unit > T 
65 
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

66 
val default: T > bool * T 
5010  67 
end; 
68 

69 
structure Position: POSITION = 

70 
struct 

71 

72 
(* datatype position *) 

73 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

74 
datatype T = Pos of (int * int * int) * Properties.T; 
41484  75 

76 
fun norm_props (props: Properties.T) = 

45666  77 
maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

78 
Markup.position_properties'; 
41484  79 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

80 
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

81 
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props}; 
27777  82 

27795  83 
fun valid (i: int) = i > 0; 
84 
fun if_valid i i' = if valid i then i' else i; 

85 

27777  86 

27796  87 
(* fields *) 
88 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

89 
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE; 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

90 
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE; 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

91 
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE; 
27796  92 

50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

93 
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; 
27796  94 

95 

27777  96 
(* advance *) 
26003  97 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

98 
fun advance_count "\n" (i: int, j: int, k: int) = 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

99 
(if_valid i (i + 1), if_valid j (j + 1), k) 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

100 
 advance_count s (i, j, k) = 
58854  101 
if Symbol.not_eof s then (i, if_valid j (j + 1), k) 
43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

102 
else (i, j, k); 
5010  103 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

104 
fun invalid_count (i, j, _: int) = 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

105 
not (valid i orelse valid j); 
27795  106 

107 
fun advance sym (pos as (Pos (count, props))) = 

108 
if invalid_count count then pos else Pos (advance_count sym count, props); 

27777  109 

68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

110 
fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) = 
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

111 
if offset = 0 orelse invalid_count count then pos 
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

112 
else if offset < 0 then raise Fail "Illegal offset" 
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset

113 
else if valid i then raise Fail "Illegal line position" 
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

114 
else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props); 
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58978
diff
changeset

115 

27777  116 

27796  117 
(* distance of adjacent positions *) 
27777  118 

68177  119 
fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) = 
120 
if valid j andalso valid j' then SOME (j'  j) else NONE; 

26882  121 

5010  122 

27777  123 
(* make position *) 
124 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

125 
val none = Pos ((0, 0, 0), []); 
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

126 
val start = Pos ((1, 1, 0), []); 
27744  127 

29307  128 

27796  129 
fun file_name "" = [] 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

130 
 file_name name = [(Markup.fileN, name)]; 
27796  131 

44200  132 
fun file_only name = Pos ((0, 0, 0), file_name name); 
43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

133 
fun file name = Pos ((1, 1, 0), file_name name); 
27744  134 

56437  135 
fun line_file_only i name = Pos ((i, 0, 0), file_name name); 
43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

136 
fun line_file i name = Pos ((i, 1, 0), file_name name); 
27795  137 
fun line i = line_file i ""; 
5010  138 

67280
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
64556
diff
changeset

139 
fun get_props (Pos (_, props)) = props; 
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
64556
diff
changeset

140 

50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

141 
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]); 
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

142 
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); 
22158  143 

50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

144 
fun get_id (Pos (_, props)) = Properties.get props Markup.idN; 
62750  145 
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props)); 
68858  146 
fun copy_id pos = (case get_id pos of NONE => I  SOME id => put_id id); 
27426  147 

63806  148 
fun parse_id pos = Option.map Value.parse_int (get_id pos); 
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50254
diff
changeset

149 

68829  150 
fun id_properties_of pos = 
151 
(case get_id pos of 

152 
SOME id => [(Markup.idN, id)] 

153 
 NONE => []); 

29307  154 

68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

155 
fun adjust_offsets adjust (pos as Pos (_, props)) = 
68858  156 
if is_none (file_of pos) then 
157 
(case parse_id pos of 

158 
SOME id => 

159 
(case adjust id of 

160 
SOME offset => 

161 
let val Pos (count, _) = advance_offsets offset pos 

162 
in Pos (count, Properties.remove Markup.idN props) end 

163 
 NONE => pos) 

164 
 NONE => pos) 

165 
else pos; 

68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

166 

6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset

167 

29307  168 
(* markup properties *) 
169 

58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

170 
fun get props name = 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

171 
(case Properties.get props name of 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

172 
NONE => 0 
63806  173 
 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

174 

25817  175 
fun of_properties props = 
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

176 
make {line = get props Markup.lineN, 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

177 
offset = get props Markup.offsetN, 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

178 
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

179 
props = props}; 
26003  180 

63806  181 
fun value k i = if valid i then [(k, Value.print_int i)] else []; 
41484  182 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
42818
diff
changeset

183 
fun properties_of (Pos ((i, j, k), props)) = 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

184 
value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props; 
26003  185 

68172  186 
fun offset_properties_of (Pos ((_, j, k), _)) = 
187 
value Markup.offsetN j @ value Markup.end_offsetN k; 

188 

54038  189 
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

190 

57899
5867d1306712
clarified signature: entity serial number is not position id;
wenzelm
parents:
56532
diff
changeset

191 
fun entity_properties_of def serial pos = 
63806  192 
if def then (Markup.defN, Value.print_int serial) :: properties_of pos 
193 
else (Markup.refN, Value.print_int serial) :: def_properties_of pos; 

45412  194 

26052  195 
fun default_properties default props = 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49691
diff
changeset

196 
if exists (member (op =) Markup.position_properties o #1) props then props 
26052  197 
else properties_of default @ props; 
198 

39440
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset

199 
val markup = Markup.properties o properties_of; 
4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset

200 

4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset

201 

4c2547af5909
simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents:
38887
diff
changeset

202 
(* 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

203 

41504  204 
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

205 
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

206 

41504  207 
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

208 
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

209 
fun report pos markup = report_text pos markup ""; 
27764  210 

44736  211 
type report = T * Markup.T; 
48767  212 
type report_text = report * string; 
44736  213 

48767  214 
val reports_text = 
215 
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

216 
#> Output.report; 
42204  217 

48767  218 
val reports = map (rpair "") #> reports_text; 
219 

44735  220 
fun store_reports _ [] _ _ = () 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset

221 
 store_reports (r: report_text list Unsynchronized.ref) ps markup x = 
42204  222 
let val ms = markup x 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55624
diff
changeset

223 
in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; 
42204  224 

55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset

225 
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

226 
Unsynchronized.change r (append (map (rpair "") reports)); 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55922
diff
changeset

227 

25817  228 

56532
3da244bc02bd
tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents:
56459
diff
changeset

229 
(* here: user output *) 
26003  230 

48992  231 
fun here pos = 
26003  232 
let 
233 
val props = properties_of pos; 

55624  234 
val (s1, s2) = 
26003  235 
(case (line_of pos, file_of pos) of 
63806  236 
(SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") 
237 
 (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") 

55624  238 
 (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") 
64556  239 
 _ => if is_reported pos then ("", "\092<^here>") else ("", "")); 
26003  240 
in 
69348  241 
if s2 = "" then "" 
55624  242 
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 
26003  243 
end; 
25817  244 

62803  245 
val here_list = implode o map here; 
49691  246 

23627  247 

27736  248 
(* range *) 
249 

250 
type range = T * T; 

251 

27796  252 
val no_range = (none, none); 
253 

62800  254 
fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); 
62797  255 
fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); 
62800  256 
fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos'); 
27777  257 

58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

258 
fun range_of_properties props = 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

259 
let 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

260 
val pos = of_properties props; 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

261 
val pos' = 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

262 
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

263 
offset = get props Markup.end_offsetN, 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

264 
end_offset = 0, 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

265 
props = props}; 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

266 
in (pos, pos') end; 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

267 

e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

268 
fun properties_of_range (pos, pos') = 
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58854
diff
changeset

269 
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

270 

27764  271 

272 
(* thread data *) 

273 

62940  274 
val thread_data = make o Thread_Position.get; 
275 
fun setmp_thread_data pos = Thread_Position.setmp (dest pos); 

27764  276 

33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset

277 
fun default pos = 
49528
789b73fcca72
report proper binding positions only  avoid swamping document model with unspecific information;
wenzelm
parents:
48992
diff
changeset

278 
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

279 
else (true, pos); 
33097
9d501e11084a
maintain position of formal entities via name space;
wenzelm
parents:
32573
diff
changeset

280 

27764  281 
end; 