wenzelm@36969
|
1 |
(* Title: Pure/Isar/token.ML
|
wenzelm@5825
|
2 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@5825
|
3 |
|
wenzelm@36969
|
4 |
Outer token syntax for Isabelle/Isar.
|
wenzelm@5825
|
5 |
*)
|
wenzelm@5825
|
6 |
|
wenzelm@36969
|
7 |
signature TOKEN =
|
wenzelm@5825
|
8 |
sig
|
wenzelm@36969
|
9 |
datatype kind =
|
wenzelm@27814
|
10 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
|
wenzelm@40536
|
11 |
Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
|
wenzelm@41206
|
12 |
Error of string | Sync | EOF
|
wenzelm@27814
|
13 |
datatype value =
|
wenzelm@27814
|
14 |
Text of string | Typ of typ | Term of term | Fact of thm list |
|
wenzelm@27814
|
15 |
Attribute of morphism -> attribute
|
wenzelm@36969
|
16 |
type T
|
wenzelm@36969
|
17 |
val str_of_kind: kind -> string
|
wenzelm@36969
|
18 |
val position_of: T -> Position.T
|
wenzelm@36969
|
19 |
val end_position_of: T -> Position.T
|
wenzelm@36969
|
20 |
val pos_of: T -> string
|
wenzelm@36969
|
21 |
val eof: T
|
wenzelm@36969
|
22 |
val is_eof: T -> bool
|
wenzelm@36969
|
23 |
val not_eof: T -> bool
|
wenzelm@36969
|
24 |
val not_sync: T -> bool
|
wenzelm@36969
|
25 |
val stopper: T Scan.stopper
|
wenzelm@36969
|
26 |
val kind_of: T -> kind
|
wenzelm@36969
|
27 |
val is_kind: kind -> T -> bool
|
wenzelm@36969
|
28 |
val keyword_with: (string -> bool) -> T -> bool
|
wenzelm@36969
|
29 |
val ident_with: (string -> bool) -> T -> bool
|
wenzelm@36969
|
30 |
val is_proper: T -> bool
|
wenzelm@36969
|
31 |
val is_semicolon: T -> bool
|
wenzelm@36969
|
32 |
val is_comment: T -> bool
|
wenzelm@36969
|
33 |
val is_begin_ignore: T -> bool
|
wenzelm@36969
|
34 |
val is_end_ignore: T -> bool
|
wenzelm@36969
|
35 |
val is_blank: T -> bool
|
wenzelm@36969
|
36 |
val is_newline: T -> bool
|
wenzelm@36969
|
37 |
val source_of: T -> string
|
wenzelm@36969
|
38 |
val source_position_of: T -> Symbol_Pos.text * Position.T
|
wenzelm@36969
|
39 |
val content_of: T -> string
|
wenzelm@36969
|
40 |
val unparse: T -> string
|
wenzelm@36969
|
41 |
val text_of: T -> string * string
|
wenzelm@36969
|
42 |
val get_value: T -> value option
|
wenzelm@36969
|
43 |
val map_value: (value -> value) -> T -> T
|
wenzelm@36969
|
44 |
val mk_text: string -> T
|
wenzelm@36969
|
45 |
val mk_typ: typ -> T
|
wenzelm@36969
|
46 |
val mk_term: term -> T
|
wenzelm@36969
|
47 |
val mk_fact: thm list -> T
|
wenzelm@36969
|
48 |
val mk_attribute: (morphism -> attribute) -> T
|
wenzelm@36969
|
49 |
val assignable: T -> T
|
wenzelm@36969
|
50 |
val assign: value option -> T -> unit
|
wenzelm@36969
|
51 |
val closure: T -> T
|
wenzelm@27814
|
52 |
val ident_or_symbolic: string -> bool
|
wenzelm@36969
|
53 |
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
|
wenzelm@27835
|
54 |
val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
|
wenzelm@36969
|
55 |
(Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
|
wenzelm@27835
|
56 |
val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
|
wenzelm@36969
|
57 |
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
|
wenzelm@30576
|
58 |
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
|
wenzelm@36969
|
59 |
val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
|
wenzelm@5825
|
60 |
end;
|
wenzelm@5825
|
61 |
|
wenzelm@36969
|
62 |
structure Token: TOKEN =
|
wenzelm@5825
|
63 |
struct
|
wenzelm@5825
|
64 |
|
wenzelm@5825
|
65 |
(** tokens **)
|
wenzelm@5825
|
66 |
|
wenzelm@27814
|
67 |
(* token values *)
|
wenzelm@27814
|
68 |
|
wenzelm@27814
|
69 |
(*The value slot assigns an (optional) internal value to a token,
|
wenzelm@27814
|
70 |
usually as a side-effect of special scanner setup (see also
|
wenzelm@27814
|
71 |
args.ML). Note that an assignable ref designates an intermediate
|
wenzelm@27814
|
72 |
state of internalization -- it is NOT meant to persist.*)
|
wenzelm@27814
|
73 |
|
wenzelm@27814
|
74 |
datatype value =
|
wenzelm@27814
|
75 |
Text of string |
|
wenzelm@27814
|
76 |
Typ of typ |
|
wenzelm@27814
|
77 |
Term of term |
|
wenzelm@27814
|
78 |
Fact of thm list |
|
wenzelm@27814
|
79 |
Attribute of morphism -> attribute;
|
wenzelm@27814
|
80 |
|
wenzelm@27814
|
81 |
datatype slot =
|
wenzelm@27814
|
82 |
Slot |
|
wenzelm@27814
|
83 |
Value of value option |
|
wenzelm@32738
|
84 |
Assignable of value option Unsynchronized.ref;
|
wenzelm@27814
|
85 |
|
wenzelm@27814
|
86 |
|
wenzelm@5825
|
87 |
(* datatype token *)
|
wenzelm@5825
|
88 |
|
wenzelm@36969
|
89 |
datatype kind =
|
wenzelm@27814
|
90 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
|
wenzelm@40536
|
91 |
Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
|
wenzelm@41206
|
92 |
Error of string | Sync | EOF;
|
wenzelm@5825
|
93 |
|
wenzelm@36969
|
94 |
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
|
wenzelm@5825
|
95 |
|
wenzelm@5825
|
96 |
val str_of_kind =
|
wenzelm@7026
|
97 |
fn Command => "command"
|
wenzelm@7026
|
98 |
| Keyword => "keyword"
|
wenzelm@5825
|
99 |
| Ident => "identifier"
|
wenzelm@5825
|
100 |
| LongIdent => "long identifier"
|
wenzelm@5825
|
101 |
| SymIdent => "symbolic identifier"
|
wenzelm@5825
|
102 |
| Var => "schematic variable"
|
wenzelm@5825
|
103 |
| TypeIdent => "type variable"
|
wenzelm@5825
|
104 |
| TypeVar => "schematic type variable"
|
wenzelm@40536
|
105 |
| Nat => "natural number"
|
wenzelm@40536
|
106 |
| Float => "floating-point number"
|
wenzelm@5825
|
107 |
| String => "string"
|
wenzelm@17164
|
108 |
| AltString => "back-quoted string"
|
wenzelm@5825
|
109 |
| Verbatim => "verbatim text"
|
wenzelm@7682
|
110 |
| Space => "white space"
|
wenzelm@7682
|
111 |
| Comment => "comment text"
|
wenzelm@27814
|
112 |
| InternalValue => "internal value"
|
wenzelm@23729
|
113 |
| Error _ => "bad input"
|
wenzelm@23788
|
114 |
| Sync => "sync marker"
|
wenzelm@5825
|
115 |
| EOF => "end-of-file";
|
wenzelm@5825
|
116 |
|
wenzelm@5825
|
117 |
|
wenzelm@27733
|
118 |
(* position *)
|
wenzelm@5825
|
119 |
|
wenzelm@27814
|
120 |
fun position_of (Token ((_, (pos, _)), _, _)) = pos;
|
wenzelm@27814
|
121 |
fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
|
wenzelm@27663
|
122 |
|
wenzelm@5825
|
123 |
val pos_of = Position.str_of o position_of;
|
wenzelm@5825
|
124 |
|
wenzelm@5825
|
125 |
|
wenzelm@27733
|
126 |
(* control tokens *)
|
wenzelm@27733
|
127 |
|
wenzelm@27814
|
128 |
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
|
wenzelm@27733
|
129 |
val eof = mk_eof Position.none;
|
wenzelm@27733
|
130 |
|
wenzelm@27814
|
131 |
fun is_eof (Token (_, (EOF, _), _)) = true
|
wenzelm@27733
|
132 |
| is_eof _ = false;
|
wenzelm@27733
|
133 |
|
wenzelm@27733
|
134 |
val not_eof = not o is_eof;
|
wenzelm@27733
|
135 |
|
wenzelm@27814
|
136 |
fun not_sync (Token (_, (Sync, _), _)) = false
|
wenzelm@27733
|
137 |
| not_sync _ = true;
|
wenzelm@27733
|
138 |
|
wenzelm@27752
|
139 |
val stopper =
|
wenzelm@27752
|
140 |
Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
|
wenzelm@27733
|
141 |
|
wenzelm@27733
|
142 |
|
wenzelm@5825
|
143 |
(* kind of token *)
|
wenzelm@5825
|
144 |
|
wenzelm@27814
|
145 |
fun kind_of (Token (_, (k, _), _)) = k;
|
wenzelm@27814
|
146 |
fun is_kind k (Token (_, (k', _), _)) = k = k';
|
wenzelm@5825
|
147 |
|
wenzelm@27814
|
148 |
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
|
wenzelm@7026
|
149 |
| keyword_with _ _ = false;
|
wenzelm@5825
|
150 |
|
wenzelm@27814
|
151 |
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
|
wenzelm@16029
|
152 |
| ident_with _ _ = false;
|
wenzelm@16029
|
153 |
|
wenzelm@27814
|
154 |
fun is_proper (Token (_, (Space, _), _)) = false
|
wenzelm@27814
|
155 |
| is_proper (Token (_, (Comment, _), _)) = false
|
wenzelm@5825
|
156 |
| is_proper _ = true;
|
wenzelm@5825
|
157 |
|
wenzelm@27814
|
158 |
fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
|
wenzelm@9130
|
159 |
| is_semicolon _ = false;
|
wenzelm@9130
|
160 |
|
wenzelm@27814
|
161 |
fun is_comment (Token (_, (Comment, _), _)) = true
|
wenzelm@17069
|
162 |
| is_comment _ = false;
|
wenzelm@17069
|
163 |
|
wenzelm@27814
|
164 |
fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
|
wenzelm@8580
|
165 |
| is_begin_ignore _ = false;
|
wenzelm@8580
|
166 |
|
wenzelm@27814
|
167 |
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
|
wenzelm@8580
|
168 |
| is_end_ignore _ = false;
|
wenzelm@8580
|
169 |
|
wenzelm@8651
|
170 |
|
wenzelm@17069
|
171 |
(* blanks and newlines -- space tokens obey lines *)
|
wenzelm@8651
|
172 |
|
wenzelm@27814
|
173 |
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
|
wenzelm@17069
|
174 |
| is_blank _ = false;
|
wenzelm@17069
|
175 |
|
wenzelm@27814
|
176 |
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
|
wenzelm@8651
|
177 |
| is_newline _ = false;
|
wenzelm@8651
|
178 |
|
wenzelm@5825
|
179 |
|
wenzelm@14991
|
180 |
(* token content *)
|
wenzelm@9155
|
181 |
|
wenzelm@44613
|
182 |
fun source_of (Token ((source, (pos, _)), (_, x), _)) =
|
wenzelm@44613
|
183 |
if YXML.detect x then x
|
wenzelm@44613
|
184 |
else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
|
wenzelm@25642
|
185 |
|
wenzelm@27885
|
186 |
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
|
wenzelm@27873
|
187 |
|
wenzelm@27814
|
188 |
fun content_of (Token (_, (_, x), _)) = x;
|
wenzelm@27747
|
189 |
|
wenzelm@27747
|
190 |
|
wenzelm@27747
|
191 |
(* unparse *)
|
wenzelm@27747
|
192 |
|
wenzelm@27814
|
193 |
fun unparse (Token (_, (kind, x), _)) =
|
wenzelm@14991
|
194 |
(case kind of
|
wenzelm@44647
|
195 |
String => Symbol_Pos.quote_string_qq x
|
wenzelm@44647
|
196 |
| AltString => Symbol_Pos.quote_string_bq x
|
wenzelm@44647
|
197 |
| Verbatim => enclose "{*" "*}" x
|
wenzelm@44647
|
198 |
| Comment => enclose "(*" "*)" x
|
wenzelm@23729
|
199 |
| Sync => ""
|
wenzelm@23729
|
200 |
| EOF => ""
|
wenzelm@14991
|
201 |
| _ => x);
|
wenzelm@14991
|
202 |
|
wenzelm@23788
|
203 |
fun text_of tok =
|
wenzelm@23788
|
204 |
if is_semicolon tok then ("terminator", "")
|
wenzelm@23729
|
205 |
else
|
wenzelm@23788
|
206 |
let
|
wenzelm@23788
|
207 |
val k = str_of_kind (kind_of tok);
|
wenzelm@40769
|
208 |
val s = unparse tok;
|
wenzelm@23788
|
209 |
in
|
wenzelm@23788
|
210 |
if s = "" then (k, "")
|
wenzelm@23788
|
211 |
else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
|
wenzelm@23788
|
212 |
else (k, s)
|
wenzelm@23788
|
213 |
end;
|
wenzelm@23729
|
214 |
|
wenzelm@5825
|
215 |
|
wenzelm@5825
|
216 |
|
wenzelm@27814
|
217 |
(** associated values **)
|
wenzelm@27814
|
218 |
|
wenzelm@27814
|
219 |
(* access values *)
|
wenzelm@27814
|
220 |
|
wenzelm@27814
|
221 |
fun get_value (Token (_, _, Value v)) = v
|
wenzelm@27814
|
222 |
| get_value _ = NONE;
|
wenzelm@27814
|
223 |
|
wenzelm@27814
|
224 |
fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
|
wenzelm@27814
|
225 |
| map_value _ tok = tok;
|
wenzelm@27814
|
226 |
|
wenzelm@27814
|
227 |
|
wenzelm@27814
|
228 |
(* make values *)
|
wenzelm@27814
|
229 |
|
wenzelm@27814
|
230 |
fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
|
wenzelm@27814
|
231 |
|
wenzelm@27814
|
232 |
val mk_text = mk_value "<text>" o Text;
|
wenzelm@27814
|
233 |
val mk_typ = mk_value "<typ>" o Typ;
|
wenzelm@27814
|
234 |
val mk_term = mk_value "<term>" o Term;
|
wenzelm@27814
|
235 |
val mk_fact = mk_value "<fact>" o Fact;
|
wenzelm@27814
|
236 |
val mk_attribute = mk_value "<attribute>" o Attribute;
|
wenzelm@27814
|
237 |
|
wenzelm@27814
|
238 |
|
wenzelm@27814
|
239 |
(* static binding *)
|
wenzelm@27814
|
240 |
|
wenzelm@27814
|
241 |
(*1st stage: make empty slots assignable*)
|
wenzelm@32738
|
242 |
fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
|
wenzelm@27814
|
243 |
| assignable tok = tok;
|
wenzelm@27814
|
244 |
|
wenzelm@27814
|
245 |
(*2nd stage: assign values as side-effect of scanning*)
|
wenzelm@27814
|
246 |
fun assign v (Token (_, _, Assignable r)) = r := v
|
wenzelm@27814
|
247 |
| assign _ _ = ();
|
wenzelm@27814
|
248 |
|
wenzelm@27814
|
249 |
(*3rd stage: static closure of final values*)
|
wenzelm@32738
|
250 |
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
|
wenzelm@27814
|
251 |
| closure tok = tok;
|
wenzelm@27814
|
252 |
|
wenzelm@27814
|
253 |
|
wenzelm@27814
|
254 |
|
wenzelm@5825
|
255 |
(** scanners **)
|
wenzelm@5825
|
256 |
|
wenzelm@30576
|
257 |
open Basic_Symbol_Pos;
|
wenzelm@27769
|
258 |
|
wenzelm@44818
|
259 |
fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
|
wenzelm@27769
|
260 |
|
wenzelm@5825
|
261 |
|
wenzelm@5825
|
262 |
(* scan symbolic idents *)
|
wenzelm@5825
|
263 |
|
wenzelm@40875
|
264 |
val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
|
wenzelm@5825
|
265 |
|
wenzelm@8231
|
266 |
val scan_symid =
|
wenzelm@40771
|
267 |
Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
|
wenzelm@40771
|
268 |
Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
|
wenzelm@5876
|
269 |
|
wenzelm@8231
|
270 |
fun is_symid str =
|
wenzelm@8231
|
271 |
(case try Symbol.explode str of
|
skalberg@15531
|
272 |
SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
|
skalberg@15531
|
273 |
| SOME ss => forall is_sym_char ss
|
wenzelm@8231
|
274 |
| _ => false);
|
wenzelm@8231
|
275 |
|
wenzelm@27814
|
276 |
fun ident_or_symbolic "begin" = false
|
wenzelm@27814
|
277 |
| ident_or_symbolic ":" = true
|
wenzelm@27814
|
278 |
| ident_or_symbolic "::" = true
|
wenzelm@43162
|
279 |
| ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
|
wenzelm@5825
|
280 |
|
wenzelm@5825
|
281 |
|
wenzelm@5825
|
282 |
(* scan verbatim text *)
|
wenzelm@5825
|
283 |
|
wenzelm@5825
|
284 |
val scan_verb =
|
wenzelm@27769
|
285 |
$$$ "*" --| Scan.ahead (~$$$ "}") ||
|
wenzelm@27769
|
286 |
Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
|
wenzelm@5825
|
287 |
|
wenzelm@5825
|
288 |
val scan_verbatim =
|
wenzelm@30576
|
289 |
(Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
|
wenzelm@30589
|
290 |
(Symbol_Pos.change_prompt
|
wenzelm@30589
|
291 |
((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
|
wenzelm@5825
|
292 |
|
wenzelm@5825
|
293 |
|
wenzelm@5825
|
294 |
(* scan space *)
|
wenzelm@5825
|
295 |
|
wenzelm@19305
|
296 |
fun is_space s = Symbol.is_blank s andalso s <> "\n";
|
wenzelm@5825
|
297 |
|
wenzelm@5825
|
298 |
val scan_space =
|
wenzelm@40771
|
299 |
Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
|
wenzelm@40771
|
300 |
Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
|
wenzelm@5825
|
301 |
|
wenzelm@5825
|
302 |
|
wenzelm@27780
|
303 |
(* scan comment *)
|
wenzelm@5825
|
304 |
|
wenzelm@5825
|
305 |
val scan_comment =
|
wenzelm@30576
|
306 |
Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
|
wenzelm@5825
|
307 |
|
wenzelm@5825
|
308 |
|
wenzelm@5825
|
309 |
|
wenzelm@27769
|
310 |
(** token sources **)
|
wenzelm@27663
|
311 |
|
wenzelm@27769
|
312 |
fun source_proper src = src |> Source.filter is_proper;
|
wenzelm@5825
|
313 |
|
wenzelm@23678
|
314 |
local
|
wenzelm@23678
|
315 |
|
wenzelm@27769
|
316 |
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
|
wenzelm@27780
|
317 |
|
wenzelm@27799
|
318 |
fun token k ss =
|
wenzelm@44580
|
319 |
Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
|
wenzelm@27799
|
320 |
|
wenzelm@27799
|
321 |
fun token_range k (pos1, (ss, pos2)) =
|
wenzelm@44580
|
322 |
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
|
wenzelm@23678
|
323 |
|
wenzelm@27769
|
324 |
fun scan (lex1, lex2) = !!! "bad input"
|
wenzelm@43374
|
325 |
(Symbol_Pos.scan_string_qq >> token_range String ||
|
wenzelm@43374
|
326 |
Symbol_Pos.scan_string_bq >> token_range AltString ||
|
wenzelm@27799
|
327 |
scan_verbatim >> token_range Verbatim ||
|
wenzelm@27799
|
328 |
scan_comment >> token_range Comment ||
|
wenzelm@27780
|
329 |
scan_space >> token Space ||
|
wenzelm@40771
|
330 |
Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
|
wenzelm@27780
|
331 |
(Scan.max token_leq
|
wenzelm@27769
|
332 |
(Scan.max token_leq
|
wenzelm@27769
|
333 |
(Scan.literal lex2 >> pair Command)
|
wenzelm@27769
|
334 |
(Scan.literal lex1 >> pair Keyword))
|
wenzelm@43162
|
335 |
(Lexicon.scan_longid >> pair LongIdent ||
|
wenzelm@43162
|
336 |
Lexicon.scan_id >> pair Ident ||
|
wenzelm@43162
|
337 |
Lexicon.scan_var >> pair Var ||
|
wenzelm@43162
|
338 |
Lexicon.scan_tid >> pair TypeIdent ||
|
wenzelm@43162
|
339 |
Lexicon.scan_tvar >> pair TypeVar ||
|
wenzelm@43162
|
340 |
Lexicon.scan_float >> pair Float ||
|
wenzelm@43162
|
341 |
Lexicon.scan_nat >> pair Nat ||
|
wenzelm@27780
|
342 |
scan_symid >> pair SymIdent) >> uncurry token));
|
wenzelm@27769
|
343 |
|
wenzelm@27769
|
344 |
fun recover msg =
|
wenzelm@40771
|
345 |
Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
|
wenzelm@27780
|
346 |
>> (single o token (Error msg));
|
wenzelm@23678
|
347 |
|
wenzelm@23678
|
348 |
in
|
wenzelm@5825
|
349 |
|
wenzelm@27835
|
350 |
fun source' {do_recover} get_lex =
|
wenzelm@30576
|
351 |
Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
|
wenzelm@27780
|
352 |
(Option.map (rpair recover) do_recover);
|
wenzelm@27780
|
353 |
|
wenzelm@5825
|
354 |
fun source do_recover get_lex pos src =
|
wenzelm@30576
|
355 |
Symbol_Pos.source pos src
|
wenzelm@27780
|
356 |
|> source' do_recover get_lex;
|
wenzelm@23678
|
357 |
|
wenzelm@23678
|
358 |
end;
|
wenzelm@5825
|
359 |
|
wenzelm@30589
|
360 |
|
wenzelm@30589
|
361 |
(* read_antiq *)
|
wenzelm@30589
|
362 |
|
wenzelm@30589
|
363 |
fun read_antiq lex scan (syms, pos) =
|
wenzelm@30589
|
364 |
let
|
wenzelm@30589
|
365 |
fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
|
wenzelm@30589
|
366 |
"@{" ^ Symbol_Pos.content syms ^ "}");
|
wenzelm@30589
|
367 |
|
wenzelm@30589
|
368 |
val res =
|
wenzelm@30589
|
369 |
Source.of_list syms
|
wenzelm@30589
|
370 |
|> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
|
wenzelm@30589
|
371 |
|> source_proper
|
wenzelm@30589
|
372 |
|> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
|
wenzelm@30589
|
373 |
|> Source.exhaust;
|
wenzelm@30589
|
374 |
in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
|
wenzelm@30589
|
375 |
|
wenzelm@5825
|
376 |
end;
|