wenzelm@5825
|
1 |
(* Title: Pure/Isar/outer_lex.ML
|
wenzelm@5825
|
2 |
ID: $Id$
|
wenzelm@5825
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@5825
|
4 |
|
wenzelm@5825
|
5 |
Outer lexical syntax for Isabelle/Isar.
|
wenzelm@5825
|
6 |
*)
|
wenzelm@5825
|
7 |
|
wenzelm@5825
|
8 |
signature OUTER_LEX =
|
wenzelm@5825
|
9 |
sig
|
wenzelm@5825
|
10 |
datatype token_kind =
|
wenzelm@23729
|
11 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
|
wenzelm@23788
|
12 |
String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF
|
aspinall@15143
|
13 |
eqtype token
|
wenzelm@5825
|
14 |
val str_of_kind: token_kind -> string
|
wenzelm@5825
|
15 |
val stopper: token * (token -> bool)
|
wenzelm@6859
|
16 |
val not_sync: token -> bool
|
wenzelm@5825
|
17 |
val not_eof: token -> bool
|
wenzelm@5825
|
18 |
val position_of: token -> Position.T
|
wenzelm@5825
|
19 |
val pos_of: token -> string
|
wenzelm@23721
|
20 |
val kind_of: token -> token_kind
|
wenzelm@5825
|
21 |
val is_kind: token_kind -> token -> bool
|
wenzelm@7026
|
22 |
val keyword_with: (string -> bool) -> token -> bool
|
wenzelm@16029
|
23 |
val ident_with: (string -> bool) -> token -> bool
|
wenzelm@5825
|
24 |
val is_proper: token -> bool
|
wenzelm@9130
|
25 |
val is_semicolon: token -> bool
|
wenzelm@17069
|
26 |
val is_comment: token -> bool
|
wenzelm@8580
|
27 |
val is_begin_ignore: token -> bool
|
wenzelm@8580
|
28 |
val is_end_ignore: token -> bool
|
wenzelm@17069
|
29 |
val is_blank: token -> bool
|
wenzelm@8651
|
30 |
val is_newline: token -> bool
|
wenzelm@14991
|
31 |
val unparse: token -> string
|
wenzelm@23788
|
32 |
val text_of: token -> string * string
|
wenzelm@5825
|
33 |
val val_of: token -> string
|
wenzelm@5876
|
34 |
val is_sid: string -> bool
|
wenzelm@9130
|
35 |
val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
|
wenzelm@9130
|
36 |
val incr_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
|
wenzelm@9130
|
37 |
val keep_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
|
wenzelm@9130
|
38 |
val scan_blank: Position.T * Symbol.symbol list
|
wenzelm@9130
|
39 |
-> Symbol.symbol * (Position.T * Symbol.symbol list)
|
wenzelm@9130
|
40 |
val scan_string: Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
|
wenzelm@7026
|
41 |
val scan: (Scan.lexicon * Scan.lexicon) ->
|
wenzelm@5825
|
42 |
Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
|
wenzelm@23721
|
43 |
val source: bool option -> (unit -> Scan.lexicon * Scan.lexicon) ->
|
wenzelm@7026
|
44 |
Position.T -> (Symbol.symbol, 'a) Source.source ->
|
wenzelm@7682
|
45 |
(token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
|
wenzelm@17164
|
46 |
val source_proper: (token, 'a) Source.source ->
|
wenzelm@17164
|
47 |
(token, (token, 'a) Source.source) Source.source
|
wenzelm@9130
|
48 |
val make_lexicon: string list -> Scan.lexicon
|
wenzelm@5825
|
49 |
end;
|
wenzelm@5825
|
50 |
|
wenzelm@5825
|
51 |
structure OuterLex: OUTER_LEX =
|
wenzelm@5825
|
52 |
struct
|
wenzelm@5825
|
53 |
|
wenzelm@5825
|
54 |
|
wenzelm@5825
|
55 |
(** tokens **)
|
wenzelm@5825
|
56 |
|
wenzelm@5825
|
57 |
(* datatype token *)
|
wenzelm@5825
|
58 |
|
wenzelm@5825
|
59 |
datatype token_kind =
|
wenzelm@23729
|
60 |
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
|
wenzelm@23788
|
61 |
String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF;
|
wenzelm@5825
|
62 |
|
wenzelm@5825
|
63 |
datatype token = Token of Position.T * (token_kind * string);
|
wenzelm@5825
|
64 |
|
wenzelm@5825
|
65 |
val str_of_kind =
|
wenzelm@7026
|
66 |
fn Command => "command"
|
wenzelm@7026
|
67 |
| Keyword => "keyword"
|
wenzelm@5825
|
68 |
| Ident => "identifier"
|
wenzelm@5825
|
69 |
| LongIdent => "long identifier"
|
wenzelm@5825
|
70 |
| SymIdent => "symbolic identifier"
|
wenzelm@5825
|
71 |
| Var => "schematic variable"
|
wenzelm@5825
|
72 |
| TypeIdent => "type variable"
|
wenzelm@5825
|
73 |
| TypeVar => "schematic type variable"
|
wenzelm@5825
|
74 |
| Nat => "number"
|
wenzelm@5825
|
75 |
| String => "string"
|
wenzelm@17164
|
76 |
| AltString => "back-quoted string"
|
wenzelm@5825
|
77 |
| Verbatim => "verbatim text"
|
wenzelm@7682
|
78 |
| Space => "white space"
|
wenzelm@7682
|
79 |
| Comment => "comment text"
|
wenzelm@23729
|
80 |
| Malformed => "malformed symbolic character"
|
wenzelm@23729
|
81 |
| Error _ => "bad input"
|
wenzelm@23788
|
82 |
| Sync => "sync marker"
|
wenzelm@5825
|
83 |
| EOF => "end-of-file";
|
wenzelm@5825
|
84 |
|
wenzelm@5825
|
85 |
|
wenzelm@10748
|
86 |
(* control tokens *)
|
wenzelm@6859
|
87 |
|
wenzelm@5825
|
88 |
val eof = Token (Position.none, (EOF, ""));
|
wenzelm@5825
|
89 |
|
wenzelm@5825
|
90 |
fun is_eof (Token (_, (EOF, _))) = true
|
wenzelm@5825
|
91 |
| is_eof _ = false;
|
wenzelm@5825
|
92 |
|
wenzelm@5825
|
93 |
val stopper = (eof, is_eof);
|
wenzelm@5825
|
94 |
val not_eof = not o is_eof;
|
wenzelm@5825
|
95 |
|
wenzelm@5825
|
96 |
|
wenzelm@23678
|
97 |
fun not_sync (Token (_, (Sync, _))) = false
|
wenzelm@23678
|
98 |
| not_sync _ = true;
|
wenzelm@23678
|
99 |
|
wenzelm@23678
|
100 |
|
wenzelm@5825
|
101 |
(* get position *)
|
wenzelm@5825
|
102 |
|
wenzelm@5825
|
103 |
fun position_of (Token (pos, _)) = pos;
|
wenzelm@5825
|
104 |
val pos_of = Position.str_of o position_of;
|
wenzelm@5825
|
105 |
|
wenzelm@5825
|
106 |
|
wenzelm@5825
|
107 |
(* kind of token *)
|
wenzelm@5825
|
108 |
|
wenzelm@23721
|
109 |
fun kind_of (Token (_, (k, _))) = k;
|
wenzelm@23721
|
110 |
|
wenzelm@5825
|
111 |
fun is_kind k (Token (_, (k', _))) = k = k';
|
wenzelm@5825
|
112 |
|
wenzelm@7026
|
113 |
fun keyword_with pred (Token (_, (Keyword, x))) = pred x
|
wenzelm@7026
|
114 |
| keyword_with _ _ = false;
|
wenzelm@5825
|
115 |
|
wenzelm@16029
|
116 |
fun ident_with pred (Token (_, (Ident, x))) = pred x
|
wenzelm@16029
|
117 |
| ident_with _ _ = false;
|
wenzelm@16029
|
118 |
|
wenzelm@7682
|
119 |
fun is_proper (Token (_, (Space, _))) = false
|
wenzelm@7682
|
120 |
| is_proper (Token (_, (Comment, _))) = false
|
wenzelm@5825
|
121 |
| is_proper _ = true;
|
wenzelm@5825
|
122 |
|
wenzelm@9195
|
123 |
fun is_semicolon (Token (_, (Keyword, ";"))) = true
|
wenzelm@9130
|
124 |
| is_semicolon _ = false;
|
wenzelm@9130
|
125 |
|
wenzelm@17069
|
126 |
fun is_comment (Token (_, (Comment, _))) = true
|
wenzelm@17069
|
127 |
| is_comment _ = false;
|
wenzelm@17069
|
128 |
|
wenzelm@8580
|
129 |
fun is_begin_ignore (Token (_, (Comment, "<"))) = true
|
wenzelm@8580
|
130 |
| is_begin_ignore _ = false;
|
wenzelm@8580
|
131 |
|
wenzelm@8580
|
132 |
fun is_end_ignore (Token (_, (Comment, ">"))) = true
|
wenzelm@8580
|
133 |
| is_end_ignore _ = false;
|
wenzelm@8580
|
134 |
|
wenzelm@8651
|
135 |
|
wenzelm@17069
|
136 |
(* blanks and newlines -- space tokens obey lines *)
|
wenzelm@8651
|
137 |
|
wenzelm@23678
|
138 |
fun is_blank (Token (_, (Space, x))) = not (String.isSuffix "\n" x)
|
wenzelm@17069
|
139 |
| is_blank _ = false;
|
wenzelm@17069
|
140 |
|
wenzelm@23678
|
141 |
fun is_newline (Token (_, (Space, x))) = String.isSuffix "\n" x
|
wenzelm@8651
|
142 |
| is_newline _ = false;
|
wenzelm@8651
|
143 |
|
wenzelm@5825
|
144 |
|
wenzelm@14991
|
145 |
(* token content *)
|
wenzelm@9155
|
146 |
|
wenzelm@18547
|
147 |
fun escape q =
|
wenzelm@18547
|
148 |
implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
|
wenzelm@18547
|
149 |
|
wenzelm@14991
|
150 |
fun unparse (Token (_, (kind, x))) =
|
wenzelm@14991
|
151 |
(case kind of
|
wenzelm@18547
|
152 |
String => x |> quote o escape "\""
|
wenzelm@18547
|
153 |
| AltString => x |> enclose "`" "`" o escape "`"
|
wenzelm@14991
|
154 |
| Verbatim => x |> enclose "{*" "*}"
|
wenzelm@14991
|
155 |
| Comment => x |> enclose "(*" "*)"
|
wenzelm@23788
|
156 |
| Malformed => Output.escape_malformed x
|
wenzelm@23729
|
157 |
| Sync => ""
|
wenzelm@23729
|
158 |
| EOF => ""
|
wenzelm@14991
|
159 |
| _ => x);
|
wenzelm@14991
|
160 |
|
wenzelm@23788
|
161 |
fun text_of tok =
|
wenzelm@23788
|
162 |
if is_semicolon tok then ("terminator", "")
|
wenzelm@23729
|
163 |
else
|
wenzelm@23788
|
164 |
let
|
wenzelm@23788
|
165 |
val k = str_of_kind (kind_of tok);
|
wenzelm@23788
|
166 |
val s = unparse tok;
|
wenzelm@23788
|
167 |
in
|
wenzelm@23788
|
168 |
if s = "" then (k, "")
|
wenzelm@23788
|
169 |
else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
|
wenzelm@23788
|
170 |
else (k, s)
|
wenzelm@23788
|
171 |
end;
|
wenzelm@23729
|
172 |
|
wenzelm@5825
|
173 |
fun val_of (Token (_, (_, x))) = x;
|
wenzelm@5825
|
174 |
|
wenzelm@5825
|
175 |
fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';
|
wenzelm@5825
|
176 |
|
wenzelm@5825
|
177 |
|
wenzelm@5825
|
178 |
|
wenzelm@5825
|
179 |
(** scanners **)
|
wenzelm@5825
|
180 |
|
wenzelm@5825
|
181 |
fun change_prompt scan = Scan.prompt "# " scan;
|
wenzelm@5825
|
182 |
|
wenzelm@5825
|
183 |
|
wenzelm@5825
|
184 |
(* diagnostics *)
|
wenzelm@5825
|
185 |
|
wenzelm@5825
|
186 |
fun lex_err msg ((pos, cs), _) = "Outer lexical error" ^ Position.str_of pos ^ ": " ^ msg cs;
|
wenzelm@9130
|
187 |
fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
|
wenzelm@5825
|
188 |
|
wenzelm@5825
|
189 |
|
wenzelm@5825
|
190 |
(* line numbering *)
|
wenzelm@5825
|
191 |
|
wenzelm@5825
|
192 |
fun incr_line scan = Scan.depend (fn pos => scan >> pair (Position.inc pos));
|
wenzelm@5825
|
193 |
val keep_line = Scan.lift;
|
wenzelm@5825
|
194 |
|
wenzelm@5825
|
195 |
val scan_blank =
|
wenzelm@5825
|
196 |
incr_line ($$ "\n") ||
|
wenzelm@5825
|
197 |
keep_line (Scan.one Symbol.is_blank);
|
wenzelm@5825
|
198 |
|
wenzelm@5825
|
199 |
|
wenzelm@5825
|
200 |
(* scan symbolic idents *)
|
wenzelm@5825
|
201 |
|
wenzelm@20664
|
202 |
val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
|
wenzelm@5825
|
203 |
|
wenzelm@8231
|
204 |
val scan_symid =
|
wenzelm@21858
|
205 |
Scan.many1 is_sym_char >> implode ||
|
wenzelm@8231
|
206 |
Scan.one Symbol.is_symbolic;
|
wenzelm@5876
|
207 |
|
wenzelm@8231
|
208 |
fun is_symid str =
|
wenzelm@8231
|
209 |
(case try Symbol.explode str of
|
skalberg@15531
|
210 |
SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
|
skalberg@15531
|
211 |
| SOME ss => forall is_sym_char ss
|
wenzelm@8231
|
212 |
| _ => false);
|
wenzelm@8231
|
213 |
|
wenzelm@20982
|
214 |
fun is_sid "begin" = false
|
wenzelm@20982
|
215 |
| is_sid ":" = true
|
wenzelm@22873
|
216 |
| is_sid "::" = true
|
wenzelm@20982
|
217 |
| is_sid s = is_symid s orelse Syntax.is_identifier s;
|
wenzelm@5825
|
218 |
|
wenzelm@5825
|
219 |
|
wenzelm@5825
|
220 |
(* scan strings *)
|
wenzelm@5825
|
221 |
|
wenzelm@17164
|
222 |
local
|
wenzelm@17164
|
223 |
|
wenzelm@17164
|
224 |
fun scan_str q =
|
wenzelm@7682
|
225 |
scan_blank ||
|
wenzelm@9130
|
226 |
keep_line ($$ "\\") |-- !!! "bad escape character in string"
|
wenzelm@17164
|
227 |
(scan_blank || keep_line ($$ q || $$ "\\")) ||
|
wenzelm@23788
|
228 |
keep_line (Scan.one (fn s => s <> q andalso s <> "\\" andalso Symbol.is_regular s));
|
wenzelm@5825
|
229 |
|
wenzelm@17164
|
230 |
fun scan_strs q =
|
wenzelm@17164
|
231 |
keep_line ($$ q) |--
|
wenzelm@9130
|
232 |
!!! "missing quote at end of string"
|
wenzelm@17164
|
233 |
(change_prompt ((Scan.repeat (scan_str q) >> implode) --| keep_line ($$ q)));
|
wenzelm@17164
|
234 |
|
wenzelm@17164
|
235 |
in
|
wenzelm@17164
|
236 |
|
wenzelm@17164
|
237 |
val scan_string = scan_strs "\"";
|
wenzelm@17164
|
238 |
val scan_alt_string = scan_strs "`";
|
wenzelm@17164
|
239 |
|
wenzelm@17164
|
240 |
end;
|
wenzelm@5825
|
241 |
|
wenzelm@5825
|
242 |
|
wenzelm@5825
|
243 |
(* scan verbatim text *)
|
wenzelm@5825
|
244 |
|
wenzelm@5825
|
245 |
val scan_verb =
|
wenzelm@5825
|
246 |
scan_blank ||
|
wenzelm@19305
|
247 |
keep_line ($$ "*" --| Scan.ahead (~$$ "}")) ||
|
wenzelm@23788
|
248 |
keep_line (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
|
wenzelm@5825
|
249 |
|
wenzelm@5825
|
250 |
val scan_verbatim =
|
wenzelm@6743
|
251 |
keep_line ($$ "{" -- $$ "*") |--
|
wenzelm@9130
|
252 |
!!! "missing end of verbatim text"
|
wenzelm@6743
|
253 |
(change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}")));
|
wenzelm@5825
|
254 |
|
wenzelm@5825
|
255 |
|
wenzelm@5825
|
256 |
(* scan space *)
|
wenzelm@5825
|
257 |
|
wenzelm@19305
|
258 |
fun is_space s = Symbol.is_blank s andalso s <> "\n";
|
wenzelm@5825
|
259 |
|
wenzelm@5825
|
260 |
val scan_space =
|
wenzelm@21858
|
261 |
(keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
|
wenzelm@21858
|
262 |
keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
|
wenzelm@5825
|
263 |
|
wenzelm@5825
|
264 |
|
wenzelm@5825
|
265 |
(* scan nested comments *)
|
wenzelm@5825
|
266 |
|
wenzelm@5825
|
267 |
val scan_cmt =
|
wenzelm@5825
|
268 |
Scan.lift scan_blank ||
|
wenzelm@5825
|
269 |
Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
|
wenzelm@5825
|
270 |
Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
|
wenzelm@19305
|
271 |
Scan.lift (keep_line ($$ "*" --| Scan.ahead (~$$ ")"))) ||
|
wenzelm@23788
|
272 |
Scan.lift (keep_line (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s)));
|
wenzelm@5825
|
273 |
|
wenzelm@5825
|
274 |
val scan_comment =
|
wenzelm@5825
|
275 |
keep_line ($$ "(" -- $$ "*") |--
|
wenzelm@9130
|
276 |
!!! "missing end of comment"
|
wenzelm@5825
|
277 |
(change_prompt
|
wenzelm@7682
|
278 |
(Scan.pass 0 (Scan.repeat scan_cmt >> implode) --| keep_line ($$ "*" -- $$ ")")));
|
wenzelm@5825
|
279 |
|
wenzelm@5825
|
280 |
|
wenzelm@23678
|
281 |
(* scan malformed symbols *)
|
wenzelm@23678
|
282 |
|
wenzelm@23678
|
283 |
local
|
wenzelm@23678
|
284 |
|
wenzelm@23678
|
285 |
val scan_mal =
|
wenzelm@23678
|
286 |
scan_blank ||
|
wenzelm@23788
|
287 |
keep_line (Scan.one Symbol.is_regular);
|
wenzelm@23678
|
288 |
|
wenzelm@23678
|
289 |
in
|
wenzelm@23678
|
290 |
|
wenzelm@23678
|
291 |
val scan_malformed =
|
wenzelm@23678
|
292 |
keep_line ($$ Symbol.malformed) |--
|
wenzelm@23729
|
293 |
change_prompt (Scan.repeat scan_mal >> implode)
|
wenzelm@23678
|
294 |
--| keep_line (Scan.option ($$ Symbol.end_malformed));
|
wenzelm@23678
|
295 |
|
wenzelm@23678
|
296 |
end;
|
wenzelm@23678
|
297 |
|
wenzelm@23678
|
298 |
|
wenzelm@5825
|
299 |
(* scan token *)
|
wenzelm@5825
|
300 |
|
wenzelm@9130
|
301 |
fun scan (lex1, lex2) =
|
wenzelm@5825
|
302 |
let
|
wenzelm@9130
|
303 |
val scanner = Scan.state :-- (fn pos =>
|
wenzelm@9130
|
304 |
let
|
wenzelm@9130
|
305 |
fun token k x = Token (pos, (k, x));
|
wenzelm@9130
|
306 |
fun sync _ = token Sync Symbol.sync;
|
wenzelm@9130
|
307 |
in
|
wenzelm@9130
|
308 |
scan_string >> token String ||
|
wenzelm@17164
|
309 |
scan_alt_string >> token AltString ||
|
wenzelm@9130
|
310 |
scan_verbatim >> token Verbatim ||
|
wenzelm@9130
|
311 |
scan_space >> token Space ||
|
wenzelm@9130
|
312 |
scan_comment >> token Comment ||
|
wenzelm@23729
|
313 |
scan_malformed >> token Malformed ||
|
wenzelm@9130
|
314 |
keep_line (Scan.one Symbol.is_sync >> sync) ||
|
wenzelm@9130
|
315 |
keep_line (Scan.max token_leq
|
wenzelm@9130
|
316 |
(Scan.max token_leq
|
wenzelm@9130
|
317 |
(Scan.literal lex1 >> (token Keyword o implode))
|
wenzelm@9130
|
318 |
(Scan.literal lex2 >> (token Command o implode)))
|
wenzelm@9130
|
319 |
(Syntax.scan_longid >> token LongIdent ||
|
wenzelm@9130
|
320 |
Syntax.scan_id >> token Ident ||
|
wenzelm@9130
|
321 |
Syntax.scan_var >> token Var ||
|
wenzelm@9130
|
322 |
Syntax.scan_tid >> token TypeIdent ||
|
wenzelm@9130
|
323 |
Syntax.scan_tvar >> token TypeVar ||
|
wenzelm@9130
|
324 |
Syntax.scan_nat >> token Nat ||
|
wenzelm@9130
|
325 |
scan_symid >> token SymIdent))
|
wenzelm@9130
|
326 |
end) >> #2;
|
wenzelm@14729
|
327 |
in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
|
wenzelm@5825
|
328 |
|
wenzelm@5825
|
329 |
|
wenzelm@9130
|
330 |
(* token sources *)
|
wenzelm@5825
|
331 |
|
wenzelm@23678
|
332 |
local
|
wenzelm@23678
|
333 |
|
wenzelm@23788
|
334 |
val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
|
wenzelm@23678
|
335 |
|
wenzelm@23682
|
336 |
fun recover msg = Scan.state :-- (fn pos =>
|
wenzelm@23729
|
337 |
keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])) >> #2;
|
wenzelm@23678
|
338 |
|
wenzelm@23678
|
339 |
in
|
wenzelm@5825
|
340 |
|
wenzelm@5825
|
341 |
fun source do_recover get_lex pos src =
|
wenzelm@5825
|
342 |
Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
|
wenzelm@23682
|
343 |
(Option.map (rpair recover) do_recover) src;
|
wenzelm@23678
|
344 |
|
wenzelm@23678
|
345 |
end;
|
wenzelm@5825
|
346 |
|
wenzelm@9130
|
347 |
fun source_proper src = src |> Source.filter is_proper;
|
wenzelm@9130
|
348 |
|
wenzelm@9130
|
349 |
|
wenzelm@9130
|
350 |
(* lexicons *)
|
wenzelm@9130
|
351 |
|
wenzelm@9130
|
352 |
val make_lexicon = Scan.make_lexicon o map Symbol.explode;
|
wenzelm@5825
|
353 |
|
wenzelm@5825
|
354 |
end;
|