equal
deleted
inserted
replaced
220 fun lex_err msg prfx (cs, _) = |
220 fun lex_err msg prfx (cs, _) = |
221 "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs); |
221 "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs); |
222 |
222 |
223 val scan_chr = |
223 val scan_chr = |
224 $$ "\\" |-- Scan.one Symbol.not_eof || |
224 $$ "\\" |-- Scan.one Symbol.not_eof || |
225 Scan.one (not_equal "'" andf Symbol.not_eof) || |
225 Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) || |
226 $$ "'" --| Scan.ahead (Scan.one (not_equal "'")); |
226 $$ "'" --| Scan.ahead (~$$ "'"); |
227 |
227 |
228 val scan_str = |
228 val scan_str = |
229 $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''") |
229 $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''") |
230 (Scan.repeat scan_chr --| $$ "'" --| $$ "'"); |
230 (Scan.repeat scan_chr --| $$ "'" --| $$ "'"); |
231 |
231 |
241 (* nested comments *) |
241 (* nested comments *) |
242 |
242 |
243 val scan_cmt = |
243 val scan_cmt = |
244 Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) || |
244 Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) || |
245 Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) || |
245 Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) || |
246 Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) || |
246 Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) || |
247 Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof)); |
247 Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s)); |
248 |
248 |
249 val scan_comment = |
249 val scan_comment = |
250 $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*") |
250 $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*") |
251 (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")") |
251 (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")") |
252 >> K (); |
252 >> K (); |