equal
deleted
inserted
replaced
234 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
234 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
235 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
235 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
236 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); |
236 Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); |
237 |
237 |
238 val scan_str = |
238 val scan_str = |
239 Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso |
239 Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso |
240 (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || |
240 (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || |
241 $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
241 $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
242 |
242 |
243 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
243 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
244 val scan_gaps = Scan.repeat scan_gap >> flat; |
244 val scan_gaps = Scan.repeat scan_gap >> flat; |