equal
deleted
inserted
replaced
168 |
168 |
169 (* scan strings *) |
169 (* scan strings *) |
170 |
170 |
171 val scan_str = |
171 val scan_str = |
172 scan_blank || |
172 scan_blank || |
173 keep_line ($$ "\\" |-- Scan.one (Symbol.not_sync andf Symbol.not_eof)) || |
173 keep_line ($$ "\\") |-- !! (lex_err (K "bad escape character in string")) |
|
174 (scan_blank || keep_line ($$ "\"" || $$ "\\")) || |
174 keep_line (Scan.one (not_equal "\\" andf not_equal "\"" andf |
175 keep_line (Scan.one (not_equal "\\" andf not_equal "\"" andf |
175 Symbol.not_sync andf Symbol.not_eof)); |
176 Symbol.not_sync andf Symbol.not_eof)); |
176 |
177 |
177 val scan_string = |
178 val scan_string = |
178 keep_line ($$ "\"") |-- |
179 keep_line ($$ "\"") |-- |