From a93528df24cf07aa67e873f3525e46f4e88e2e32 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 29 Jun 2017 14:25:59 +0200 Subject: [PATCH] fix(leanpkg): read carriage-return as whitespace --- leanpkg/leanpkg/toml.lean | 2 +- library/data/buffer/parser.lean | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/leanpkg/leanpkg/toml.lean b/leanpkg/leanpkg/toml.lean index 3742ddb39e..341183b714 100644 --- a/leanpkg/leanpkg/toml.lean +++ b/leanpkg/leanpkg/toml.lean @@ -78,7 +78,7 @@ ch '#' >> many' (sat (≠ '#')) >> optional (ch '\n') >> eps def Ws : parser unit := decorate_error "" $ -many' $ one_of' " \t\n".to_list <|> Comment +many' $ one_of' " \t\x0d\n".to_list <|> Comment def tok (s : string) := str s >> Ws diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean index 06b9475d01..ff811e657b 100644 --- a/library/data/buffer/parser.lean +++ b/library/data/buffer/parser.lean @@ -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 :=