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