fix(leanpkg): read carriage-return as whitespace
This commit is contained in:
parent
ee94f7688c
commit
a93528df24
2 changed files with 2 additions and 1 deletions
|
|
@ -78,7 +78,7 @@ ch '#' >> many' (sat (≠ '#')) >> optional (ch '\n') >> eps
|
|||
|
||||
def Ws : parser unit :=
|
||||
decorate_error "<whitespace>" $
|
||||
many' $ one_of' " \t\n".to_list <|> Comment
|
||||
many' $ one_of' " \t\x0d\n".to_list <|> Comment
|
||||
|
||||
def tok (s : string) := str s >> Ws
|
||||
|
||||
|
|
|
|||
|
|
@ -181,6 +181,7 @@ def fix (F : parser α → parser α) : parser α :=
|
|||
private def make_monospaced : char → char
|
||||
| '\n' := ' '
|
||||
| '\t' := ' '
|
||||
| '\x0d' := ' '
|
||||
| c := c
|
||||
|
||||
def mk_error_msg (input : char_buffer) (pos : ℕ) (expected : dlist string) : char_buffer :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue