author | wenzelm |
Sun, 14 Jan 2018 14:11:02 +0100 | |
changeset 67425 | 7d4a088dbc0e |
parent 67363 | 408a137e2793 |
child 67427 | 5409cfd41e7f |
permissions | -rw-r--r-- |
24579 | 1 |
(* Title: Pure/ML/ml_lex.ML |
2 |
Author: Makarius |
|
3 |
||
59109 | 4 |
Lexical syntax for Isabelle/ML and Standard ML. |
24579 | 5 |
*) |
6 |
||
7 |
signature ML_LEX = |
|
8 |
sig |
|
55505 | 9 |
val keywords: string list |
24579 | 10 |
datatype token_kind = |
59082 | 11 |
Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | |
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
12 |
Space | Comment of Comment.kind option | Error of string | EOF |
24579 | 13 |
eqtype token |
27732 | 14 |
val stopper: token Scan.stopper |
24596 | 15 |
val is_regular: token -> bool |
16 |
val is_improper: token -> bool |
|
67362 | 17 |
val is_comment: token -> bool |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
18 |
val set_range: Position.range -> token -> token |
59112 | 19 |
val range_of: token -> Position.range |
30636 | 20 |
val pos_of: token -> Position.T |
31474 | 21 |
val end_pos_of: token -> Position.T |
24579 | 22 |
val kind_of: token -> token_kind |
27817 | 23 |
val content_of: token -> string |
31426 | 24 |
val check_content_of: token -> string |
31332 | 25 |
val flatten: token list -> string |
24596 | 26 |
val source: (Symbol.symbol, 'a) Source.source -> |
30573 | 27 |
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) |
27772 | 28 |
Source.source) Source.source |
30591 | 29 |
val tokenize: string -> token list |
59067 | 30 |
val read_pos: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list |
31 |
val read: Symbol_Pos.text -> token Antiquote.antiquote list |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58933
diff
changeset
|
32 |
val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list |
59064 | 33 |
val read_source: bool -> Input.source -> token Antiquote.antiquote list |
24579 | 34 |
end; |
35 |
||
36 |
structure ML_Lex: ML_LEX = |
|
37 |
struct |
|
38 |
||
55505 | 39 |
(** keywords **) |
40 |
||
41 |
val keywords = |
|
42 |
["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[", |
|
43 |
"]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case", |
|
44 |
"datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun", |
|
45 |
"functor", "handle", "if", "in", "include", "infix", "infixr", |
|
46 |
"let", "local", "nonfix", "of", "op", "open", "orelse", "raise", |
|
47 |
"rec", "sharing", "sig", "signature", "struct", "structure", "then", |
|
48 |
"type", "val", "where", "while", "with", "withtype"]; |
|
49 |
||
50 |
val keywords2 = |
|
58933 | 51 |
["and", "case", "do", "else", "end", "if", "in", "let", "local", "of", |
55505 | 52 |
"sig", "struct", "then", "while", "with"]; |
53 |
||
54 |
val keywords3 = |
|
55 |
["handle", "open", "raise"]; |
|
56 |
||
57 |
val lexicon = Scan.make_lexicon (map raw_explode keywords); |
|
58 |
||
59 |
||
60 |
||
24579 | 61 |
(** tokens **) |
62 |
||
63 |
(* datatype token *) |
|
64 |
||
65 |
datatype token_kind = |
|
59082 | 66 |
Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | |
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
67 |
Space | Comment of Comment.kind option | Error of string | EOF; |
24579 | 68 |
|
27772 | 69 |
datatype token = Token of Position.range * (token_kind * string); |
70 |
||
71 |
||
72 |
(* position *) |
|
73 |
||
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
74 |
fun set_range range (Token (_, x)) = Token (range, x); |
59112 | 75 |
fun range_of (Token (range, _)) = range; |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
76 |
|
59112 | 77 |
val pos_of = #1 o range_of; |
78 |
val end_pos_of = #2 o range_of; |
|
24579 | 79 |
|
80 |
||
58855 | 81 |
(* stopper *) |
24579 | 82 |
|
27772 | 83 |
fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); |
84 |
val eof = mk_eof Position.none; |
|
24579 | 85 |
|
86 |
fun is_eof (Token (_, (EOF, _))) = true |
|
87 |
| is_eof _ = false; |
|
88 |
||
27772 | 89 |
val stopper = |
30636 | 90 |
Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; |
27772 | 91 |
|
24579 | 92 |
|
27772 | 93 |
(* token content *) |
94 |
||
31426 | 95 |
fun kind_of (Token (_, (k, _))) = k; |
96 |
||
27817 | 97 |
fun content_of (Token (_, (_, x))) = x; |
98 |
fun token_leq (tok, tok') = content_of tok <= content_of tok'; |
|
27772 | 99 |
|
55505 | 100 |
fun is_keyword (Token (_, (Keyword, _))) = true |
101 |
| is_keyword _ = false; |
|
102 |
||
103 |
fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) |
|
104 |
| is_delimiter _ = false; |
|
105 |
||
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
106 |
fun is_regular (Token (_, (Error _, _))) = false |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
107 |
| is_regular (Token (_, (EOF, _))) = false |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
108 |
| is_regular _ = true; |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
109 |
|
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
110 |
fun is_improper (Token (_, (Space, _))) = true |
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
111 |
| is_improper (Token (_, (Comment _, _))) = true |
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
112 |
| is_improper _ = false; |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
113 |
|
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
114 |
fun is_comment (Token (_, (Comment _, _))) = true |
67362 | 115 |
| is_comment _ = false; |
116 |
||
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
117 |
fun warn tok = |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
118 |
(case tok of |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
119 |
Token (_, (Keyword, ":>")) => |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
120 |
warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
121 |
\prefer non-opaque matching (:) possibly with abstype" ^ |
48992 | 122 |
Position.here (pos_of tok)) |
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
123 |
| _ => ()); |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
124 |
|
31426 | 125 |
fun check_content_of tok = |
30636 | 126 |
(case kind_of tok of |
30645 | 127 |
Error msg => error msg |
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
128 |
| _ => content_of tok); |
30636 | 129 |
|
59112 | 130 |
|
131 |
(* flatten *) |
|
132 |
||
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
133 |
fun flatten_content (tok :: (toks as tok' :: _)) = |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
134 |
Symbol.escape (check_content_of tok) :: |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
135 |
(if is_improper tok orelse is_improper tok' then flatten_content toks |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
136 |
else Symbol.space :: flatten_content toks) |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
137 |
| flatten_content toks = map (Symbol.escape o check_content_of) toks; |
31332 | 138 |
|
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
139 |
val flatten = implode o flatten_content; |
24596 | 140 |
|
141 |
||
30614 | 142 |
(* markup *) |
143 |
||
37195 | 144 |
local |
145 |
||
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
146 |
fun token_kind_markup SML = |
59124 | 147 |
fn Type_Var => (Markup.ML_tvar, "") |
59082 | 148 |
| Word => (Markup.ML_numeral, "") |
149 |
| Int => (Markup.ML_numeral, "") |
|
150 |
| Real => (Markup.ML_numeral, "") |
|
151 |
| Char => (Markup.ML_char, "") |
|
152 |
| String => (if SML then Markup.SML_string else Markup.ML_string, "") |
|
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
153 |
| Comment _ => (if SML then Markup.SML_comment else Markup.ML_comment, "") |
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
64275
diff
changeset
|
154 |
| Error msg => (Markup.bad (), msg) |
59124 | 155 |
| _ => (Markup.empty, ""); |
30614 | 156 |
|
37195 | 157 |
in |
158 |
||
61457 | 159 |
fun token_report SML (tok as Token ((pos, _), (kind, x))) = |
55505 | 160 |
let |
161 |
val (markup, txt) = |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
162 |
if not (is_keyword tok) then token_kind_markup SML kind |
55505 | 163 |
else if is_delimiter tok then (Markup.ML_delimiter, "") |
66067 | 164 |
else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "") |
165 |
else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "") |
|
166 |
else (Markup.ML_keyword1 |> Markup.keyword_properties, ""); |
|
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
167 |
in ((pos, markup), txt) end; |
37195 | 168 |
|
169 |
end; |
|
30614 | 170 |
|
171 |
||
24579 | 172 |
|
173 |
(** scanners **) |
|
174 |
||
30573 | 175 |
open Basic_Symbol_Pos; |
24579 | 176 |
|
55105 | 177 |
val err_prefix = "SML lexical error: "; |
178 |
||
179 |
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); |
|
24579 | 180 |
|
181 |
||
182 |
(* identifiers *) |
|
183 |
||
24596 | 184 |
local |
185 |
||
24579 | 186 |
val scan_letdigs = |
55496 | 187 |
Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol); |
24579 | 188 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
189 |
val scan_alphanumeric = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61596
diff
changeset
|
190 |
Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs; |
24579 | 191 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
192 |
val scan_symbolic = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40525
diff
changeset
|
193 |
Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol); |
24579 | 194 |
|
24596 | 195 |
in |
196 |
||
24579 | 197 |
val scan_ident = scan_alphanumeric || scan_symbolic; |
198 |
||
55496 | 199 |
val scan_long_ident = |
61476 | 200 |
Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "="); |
24579 | 201 |
|
55496 | 202 |
val scan_type_var = $$$ "'" @@@ scan_letdigs; |
24579 | 203 |
|
24596 | 204 |
end; |
24579 | 205 |
|
206 |
||
207 |
(* numerals *) |
|
208 |
||
24596 | 209 |
local |
210 |
||
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
211 |
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol); |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
212 |
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); |
27772 | 213 |
val scan_sign = Scan.optional ($$$ "~") []; |
214 |
val scan_decint = scan_sign @@@ scan_dec; |
|
55496 | 215 |
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint; |
24579 | 216 |
|
24596 | 217 |
in |
218 |
||
27772 | 219 |
val scan_word = |
220 |
$$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex || |
|
221 |
$$$ "0" @@@ $$$ "w" @@@ scan_dec; |
|
24579 | 222 |
|
27772 | 223 |
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec); |
24579 | 224 |
|
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
225 |
val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) []; |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
226 |
|
24579 | 227 |
val scan_real = |
27772 | 228 |
scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] || |
229 |
scan_decint @@@ scan_exp; |
|
24579 | 230 |
|
24596 | 231 |
end; |
232 |
||
24579 | 233 |
|
234 |
(* chars and strings *) |
|
235 |
||
55496 | 236 |
val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol); |
237 |
||
24596 | 238 |
local |
239 |
||
240 |
val scan_escape = |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40525
diff
changeset
|
241 |
Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single || |
64275
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
63936
diff
changeset
|
242 |
$$$ "^" @@@ |
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
63936
diff
changeset
|
243 |
(Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
244 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
245 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
246 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); |
24596 | 247 |
|
248 |
val scan_str = |
|
58854 | 249 |
Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso |
30600
de241396389c
allow non-printable symbols within string tokens;
wenzelm
parents:
30593
diff
changeset
|
250 |
(not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || |
27772 | 251 |
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
24596 | 252 |
|
27772 | 253 |
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
61476 | 254 |
val scan_gaps = Scan.repeats scan_gap; |
24579 | 255 |
|
24596 | 256 |
in |
24579 | 257 |
|
258 |
val scan_char = |
|
27772 | 259 |
$$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; |
24579 | 260 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
261 |
val recover_char = |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
262 |
$$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
263 |
|
24579 | 264 |
val scan_string = |
55103 | 265 |
Scan.ahead ($$ "\"") |-- |
266 |
!!! "unclosed string literal" |
|
61476 | 267 |
($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\""); |
24596 | 268 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
269 |
val recover_string = |
61476 | 270 |
$$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str); |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
271 |
|
24596 | 272 |
end; |
24579 | 273 |
|
274 |
||
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
275 |
(* rat antiquotation *) |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
276 |
|
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
277 |
val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none); |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
278 |
|
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
279 |
val scan_rat_antiq = |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
280 |
Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
281 |
>> (fn ((pos1, (pos2, body)), pos3) => |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
282 |
{start = Position.range_position (pos1, pos2), |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
283 |
stop = Position.none, |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
284 |
range = Position.range (pos1, pos3), |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
285 |
body = rat_name @ body}); |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
286 |
|
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
287 |
|
30645 | 288 |
(* scan tokens *) |
24579 | 289 |
|
290 |
local |
|
291 |
||
30593 | 292 |
fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); |
24579 | 293 |
|
30593 | 294 |
val scan_ml = |
27772 | 295 |
(scan_char >> token Char || |
296 |
scan_string >> token String || |
|
297 |
scan_blanks1 >> token Space || |
|
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
298 |
Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || |
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67363
diff
changeset
|
299 |
Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) || |
27772 | 300 |
Scan.max token_leq |
55505 | 301 |
(Scan.literal lexicon >> token Keyword) |
27772 | 302 |
(scan_word >> token Word || |
303 |
scan_real >> token Real || |
|
304 |
scan_int >> token Int || |
|
59082 | 305 |
scan_long_ident >> token Long_Ident || |
27772 | 306 |
scan_ident >> token Ident || |
59082 | 307 |
scan_type_var >> token Type_Var)); |
27772 | 308 |
|
59112 | 309 |
val scan_sml = scan_ml >> Antiquote.Text; |
310 |
||
311 |
val scan_ml_antiq = |
|
61471 | 312 |
Antiquote.scan_control >> Antiquote.Control || |
59112 | 313 |
Antiquote.scan_antiq >> Antiquote.Antiq || |
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
62797
diff
changeset
|
314 |
scan_rat_antiq >> Antiquote.Antiq || |
59112 | 315 |
scan_ml >> Antiquote.Text; |
30645 | 316 |
|
27772 | 317 |
fun recover msg = |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
318 |
(recover_char || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
319 |
recover_string || |
59112 | 320 |
Symbol_Pos.recover_cartouche || |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
321 |
Symbol_Pos.recover_comment || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
322 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
323 |
>> (single o token (Error msg)); |
24579 | 324 |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
325 |
fun gen_read SML pos text = |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37195
diff
changeset
|
326 |
let |
59110
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
59109
diff
changeset
|
327 |
val syms = |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
59109
diff
changeset
|
328 |
Symbol_Pos.explode (text, pos) |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
59109
diff
changeset
|
329 |
|> SML ? maps (fn (s, p) => raw_explode s |> map (rpair p)); |
8a78c7cb5b14
some special cases for official SML, to treat Isabelle symbols like raw characters;
wenzelm
parents:
59109
diff
changeset
|
330 |
|
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
331 |
val termination = |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
332 |
if null syms then [] |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
333 |
else |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
334 |
let |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
335 |
val pos1 = List.last syms |-> Position.advance; |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
336 |
val pos2 = Position.advance Symbol.space pos1; |
62797 | 337 |
in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end; |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
338 |
|
59112 | 339 |
val scan = if SML then scan_sml else scan_ml_antiq; |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
340 |
fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok) |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
341 |
| check _ = (); |
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
342 |
val input = |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
343 |
Source.of_list syms |
58864 | 344 |
|> Source.source Symbol_Pos.stopper |
345 |
(Scan.recover (Scan.bulk (!!! "bad input" scan)) |
|
346 |
(fn msg => recover msg >> map Antiquote.Text)) |
|
61482 | 347 |
|> Source.exhaust; |
348 |
val _ = Position.reports (Antiquote.antiq_reports input); |
|
349 |
val _ = |
|
350 |
Position.reports_text (maps (fn Antiquote.Text t => [token_report SML t] | _ => []) input); |
|
351 |
val _ = List.app check input; |
|
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
352 |
in input @ termination end; |
30645 | 353 |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
354 |
in |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
355 |
|
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
356 |
fun source src = |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
357 |
Symbol_Pos.source (Position.line 1) src |
58864 | 358 |
|> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover); |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
359 |
|
63936 | 360 |
val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust; |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
361 |
|
59067 | 362 |
val read_pos = gen_read false; |
363 |
||
364 |
val read = read_pos Position.none; |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55828
diff
changeset
|
365 |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58933
diff
changeset
|
366 |
fun read_set_range range = |
59067 | 367 |
read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq); |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58933
diff
changeset
|
368 |
|
59064 | 369 |
fun read_source SML source = |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56278
diff
changeset
|
370 |
let |
59064 | 371 |
val pos = Input.pos_of source; |
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56278
diff
changeset
|
372 |
val language = if SML then Markup.language_SML else Markup.language_ML; |
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56278
diff
changeset
|
373 |
val _ = |
59064 | 374 |
if Position.is_reported_range pos |
375 |
then Position.report pos (language (Input.is_delimited source)) |
|
56459
38d0b2099743
no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents:
56278
diff
changeset
|
376 |
else (); |
59064 | 377 |
in gen_read SML pos (Input.text_of source) end; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55612
diff
changeset
|
378 |
|
24579 | 379 |
end; |
380 |
||
24596 | 381 |
end; |