202 fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); |
202 fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); |
203 |
203 |
204 fun reports_of_block pos = |
204 fun reports_of_block pos = |
205 [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)]; |
205 [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)]; |
206 |
206 |
207 fun reports_of (xsym, pos: Position.T) = |
207 fun reports_of (xsym, pos) = |
208 (case xsym of |
208 (case xsym of |
209 Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)] |
209 Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)] |
210 | Argument _ => [(pos, Markup.expression "mixfix argument")] |
210 | Argument _ => [(pos, Markup.expression "mixfix argument")] |
211 | Space _ => [(pos, Markup.expression "mixfix space")] |
211 | Space _ => [(pos, Markup.expression "mixfix space")] |
212 | Bg _ => reports_of_block pos |
212 | Bg _ => reports_of_block pos |
213 | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)] |
213 | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)] |
214 | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]); |
214 | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]); |
|
215 |
|
216 fun reports_text_of (xsym, pos) = |
|
217 (case xsym of |
|
218 Delim s => |
|
219 if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then |
|
220 [((pos, Markup.bad), |
|
221 "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")] |
|
222 else [] |
|
223 | _ => []); |
215 |
224 |
216 fun read_block_properties ss = |
225 fun read_block_properties ss = |
217 let |
226 let |
218 val props = read_properties ss; |
227 val props = read_properties ss; |
219 |
228 |
271 val xsymbs = |
280 val xsymbs = |
272 (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of |
281 (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of |
273 (res, []) => map_filter I res |
282 (res, []) => map_filter I res |
274 | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); |
283 | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); |
275 val _ = Position.reports (maps reports_of xsymbs); |
284 val _ = Position.reports (maps reports_of xsymbs); |
|
285 val _ = Position.reports_text (maps reports_text_of xsymbs); |
276 in xsymbs end; |
286 in xsymbs end; |
277 |
287 |
278 val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none)); |
288 val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none)); |
279 val mixfix_args = mfix_args o Input.source_explode; |
289 val mixfix_args = mfix_args o Input.source_explode; |
280 |
290 |