equal
deleted
inserted
replaced
161 Scan.one (Symbol.is_ascii_digit o symbol) -- |
161 Scan.one (Symbol.is_ascii_digit o symbol) -- |
162 Scan.one (Symbol.is_ascii_digit o symbol) -- |
162 Scan.one (Symbol.is_ascii_digit o symbol) -- |
163 Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]); |
163 Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]); |
164 |
164 |
165 val scan_str = |
165 val scan_str = |
166 Scan.one (fn (s, _) => Symbol.is_regular s andalso Symbol.is_printable s |
166 Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso |
167 andalso s <> "\"" andalso s <> "\\") >> single || |
167 (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || |
168 $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
168 $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
169 |
169 |
170 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
170 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
171 val scan_gaps = Scan.repeat scan_gap >> flat; |
171 val scan_gaps = Scan.repeat scan_gap >> flat; |
172 |
172 |