author | wenzelm |
Fri, 09 Apr 2021 22:06:59 +0200 | |
changeset 73550 | 2f6855142a8c |
parent 69891 | def3ec9cdb7e |
child 73551 | 53c148e39819 |
permissions | -rw-r--r-- |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
1 |
(* Title: Pure/General/antiquote.ML |
55511
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
wenzelm
parents:
55107
diff
changeset
|
2 |
Author: Makarius |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
3 |
|
55511
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
wenzelm
parents:
55107
diff
changeset
|
4 |
Antiquotations within plain text. |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
5 |
*) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
6 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
7 |
signature ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
8 |
sig |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
9 |
type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list} |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
10 |
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list} |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
11 |
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq |
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
12 |
val the_text: 'a antiquote -> 'a |
61434 | 13 |
type text_antiquote = Symbol_Pos.T list antiquote |
67467 | 14 |
val text_antiquote_range: text_antiquote -> Position.range |
15 |
val text_range: text_antiquote list -> Position.range |
|
61434 | 16 |
val split_lines: text_antiquote list -> text_antiquote list list |
61457 | 17 |
val antiq_reports: 'a antiquote list -> Position.report list |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
18 |
val update_reports: bool -> Position.T -> string list -> Position.report_text list |
67426 | 19 |
val scan_control: control scanner |
20 |
val scan_antiq: antiq scanner |
|
21 |
val scan_antiquote: text_antiquote scanner |
|
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
22 |
val scan_antiquote_comments: text_antiquote scanner |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
23 |
val parse_comments: Position.T -> Symbol_Pos.T list -> text_antiquote list |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
24 |
val read_comments: Input.source -> text_antiquote list |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
25 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
26 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
27 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
28 |
struct |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
29 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
30 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
31 |
|
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
32 |
type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}; |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
33 |
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}; |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
34 |
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
35 |
|
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
36 |
fun bad_text pos = error ("Unexpected antiquotation" ^ Position.here pos); |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
37 |
fun the_text (Text x) = x |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
38 |
| the_text (Control {range, ...}) = bad_text (#1 range) |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
39 |
| the_text (Antiq {range, ...}) = bad_text (#1 range); |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
69891
diff
changeset
|
40 |
|
61434 | 41 |
type text_antiquote = Symbol_Pos.T list antiquote; |
42 |
||
67467 | 43 |
fun text_antiquote_range (Text ss) = Symbol_Pos.range ss |
44 |
| text_antiquote_range (Control {range, ...}) = range |
|
45 |
| text_antiquote_range (Antiq {range, ...}) = range; |
|
61450 | 46 |
|
67467 | 47 |
fun text_range ants = |
61450 | 48 |
if null ants then Position.no_range |
67467 | 49 |
else |
50 |
Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants))); |
|
61450 | 51 |
|
61434 | 52 |
|
53 |
(* split lines *) |
|
54 |
||
55 |
fun split_lines input = |
|
56 |
let |
|
57 |
fun add a (line, lines) = (a :: line, lines); |
|
58 |
fun flush (line, lines) = ([], rev line :: lines); |
|
59 |
fun split (a as Text ss) = |
|
67522 | 60 |
(case chop_prefix (fn ("\n", _) => false | _ => true) ss of |
61434 | 61 |
([], []) => I |
62 |
| (_, []) => add a |
|
63 |
| ([], _ :: rest) => flush #> split (Text rest) |
|
64 |
| (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest)) |
|
65 |
| split a = add a; |
|
61440 | 66 |
in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end; |
61434 | 67 |
|
27342 | 68 |
|
44736 | 69 |
(* reports *) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
70 |
|
61457 | 71 |
fun antiq_reports ants = ants |> maps |
61471 | 72 |
(fn Text _ => [] |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
73 |
| Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)] |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
74 |
| Antiq {start, stop, range = (pos, _), ...} => |
61471 | 75 |
[(start, Markup.antiquote), |
76 |
(stop, Markup.antiquote), |
|
77 |
(pos, Markup.antiquoted), |
|
78 |
(pos, Markup.language_antiquotation)]); |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
79 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
80 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
81 |
(* update *) |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
82 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
83 |
fun update_reports embedded pos src = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
84 |
let |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
85 |
val n = length src; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
86 |
val no_arg = n = 1; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
87 |
val embedded_arg = n = 2 andalso embedded; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
88 |
val control = |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
89 |
(case src of |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
90 |
name :: _ => |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
91 |
if Symbol.is_ascii_identifier name andalso name <> "cartouche" andalso |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
92 |
(no_arg orelse embedded_arg) |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
93 |
then SOME (Symbol.control_prefix ^ name ^ Symbol.control_suffix) |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
94 |
else NONE |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
95 |
| [] => NONE); |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
96 |
val arg = if embedded_arg then cartouche (nth src 1) else ""; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
97 |
in |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
98 |
(case control of |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
99 |
SOME sym => [((pos, Markup.update), sym ^ arg)] |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
100 |
| NONE => []) |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
101 |
end; |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
102 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
103 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
67735
diff
changeset
|
104 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
105 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
106 |
|
30573 | 107 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
108 |
|
22114 | 109 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
110 |
|
48764 | 111 |
val err_prefix = "Antiquotation lexical error: "; |
112 |
||
67193 | 113 |
val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single; |
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
114 |
val scan_nl_opt = Scan.optional scan_nl []; |
67193 | 115 |
|
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
116 |
val scan_plain_txt = |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
117 |
Scan.many1 (fn (s, _) => |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
118 |
not (Comment.is_symbol s) andalso |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
119 |
not (Symbol.is_control s) andalso |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
120 |
s <> Symbol.open_ andalso |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
121 |
s <> "@" andalso |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
122 |
s <> "\n" andalso |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
123 |
Symbol.not_eof s) || |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
124 |
Scan.one (Comment.is_symbol o Symbol_Pos.symbol) >> single || |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
125 |
$$$ "@" --| Scan.ahead (~$$ "{"); |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
126 |
|
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
127 |
val scan_text = |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
128 |
scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt; |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
129 |
|
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
130 |
val scan_text_comments = |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
69592
diff
changeset
|
131 |
scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
132 |
|
55512 | 133 |
val scan_antiq_body = |
48764 | 134 |
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
61481 | 135 |
Symbol_Pos.scan_cartouche err_prefix || |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
69592
diff
changeset
|
136 |
Comment.scan_inner -- |
67735
e2e002d4a4de
clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
wenzelm
parents:
67571
diff
changeset
|
137 |
Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail |
e2e002d4a4de
clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
wenzelm
parents:
67571
diff
changeset
|
138 |
>> K [] || |
58854 | 139 |
Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
140 |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
141 |
fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name); |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
142 |
|
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
143 |
in |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
144 |
|
61471 | 145 |
val scan_control = |
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
146 |
Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) -- |
61481 | 147 |
Symbol_Pos.scan_cartouche err_prefix >> |
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
148 |
(fn (opt_control, body) => |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
149 |
let |
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
150 |
val (name, range) = |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
151 |
(case opt_control of |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
152 |
SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body)) |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61481
diff
changeset
|
153 |
| NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body)); |
61595 | 154 |
in {name = name, range = range, body = body} end) || |
155 |
Scan.one (Symbol.is_control o Symbol_Pos.symbol) >> |
|
156 |
(fn (sym, pos) => |
|
157 |
{name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []}); |
|
61471 | 158 |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
159 |
val scan_antiq = |
55526 | 160 |
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
48764 | 161 |
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
61476 | 162 |
(Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> |
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
163 |
(fn (pos1, (pos2, ((body, pos3), pos4))) => |
62797 | 164 |
{start = Position.range_position (pos1, pos2), |
165 |
stop = Position.range_position (pos3, pos4), |
|
166 |
range = Position.range (pos1, pos4), |
|
61476 | 167 |
body = body}); |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
168 |
|
61471 | 169 |
val scan_antiquote = |
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
170 |
scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq; |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
171 |
|
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
172 |
val scan_antiquote_comments = |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
173 |
scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
174 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
175 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
176 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
177 |
|
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
178 |
(* parse and read (with formal comments) *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
179 |
|
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
180 |
fun parse_comments pos syms = |
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
181 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote_comments) syms of |
62749 | 182 |
SOME ants => ants |
61456 | 183 |
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); |
184 |
||
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
185 |
fun read_comments source = |
62749 | 186 |
let |
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67522
diff
changeset
|
187 |
val ants = parse_comments (Input.pos_of source) (Input.source_explode source); |
62749 | 188 |
val _ = Position.reports (antiq_reports ants); |
189 |
in ants end; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
190 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
191 |
end; |