equal
deleted
inserted
replaced
71 scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig) || |
71 scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig) || |
72 (Scan.repeat1 scan_blank >> implode) ^^ keep_line ($$ "\\")); |
72 (Scan.repeat1 scan_blank >> implode) ^^ keep_line ($$ "\\")); |
73 |
73 |
74 val scan_str = |
74 val scan_str = |
75 scan_esc || |
75 scan_esc || |
76 scan_blank >> K " " || |
76 scan_blank >> K Symbol.space || |
77 keep_line (Scan.one (not_equal "\"" andf Symbol.not_eof)); |
77 keep_line (Scan.one (not_equal "\"" andf Symbol.not_eof)); |
78 |
78 |
79 val scan_string = |
79 val scan_string = |
80 keep_line ($$ "\"") ^^ |
80 keep_line ($$ "\"") ^^ |
81 !! (fn ((n, _), _) => lex_err n "missing quote at end of string") |
81 !! (fn ((n, _), _) => lex_err n "missing quote at end of string") |