equal
deleted
inserted
replaced
30 |
30 |
31 |
31 |
32 (* reports *) |
32 (* reports *) |
33 |
33 |
34 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) = |
34 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) = |
35 [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)]; |
35 [(start, Markup.antiquote), (stop, Markup.antiquote), |
|
36 (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)]; |
36 |
37 |
37 fun antiquote_reports text = |
38 fun antiquote_reports text = |
38 maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq)); |
39 maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq)); |
39 |
40 |
40 |
41 |