From dd6e95c7189fbcc3a8a1edfc5e1bf5e40b406aca Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sun, 12 Jan 2020 13:53:34 -0500 Subject: [PATCH] fix: lowercase error messages --- src/Init/System/IOError.lean | 10 +++++----- tests/lean/file_not_found.lean.expected.out | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 3f87126dd7..e97905f1d8 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -152,16 +152,16 @@ timeExpired private def downCaseFirst (s : String) : String := s.modify 0 Char.toLower def fopenErrorToString (gist fn : String) (code : UInt32) : Option String → String -| some details => gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")\n file: " ++ fn -| none => gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn +| some details => downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")\n file: " ++ fn +| none => downCaseFirst gist ++ " (error code: " ++ toString code ++ ")\n file: " ++ fn def otherErrorToString (gist : String) (code : UInt32) : Option String → String -| some details => gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")" -| none => gist ++ " (error code: " ++ toString code ++ ")" +| some details => downCaseFirst gist ++ " (error code: " ++ toString code ++ ", " ++ downCaseFirst details ++ ")" +| none => downCaseFirst gist ++ " (error code: " ++ toString code ++ ")" @[export lean_io_error_to_string] def toString : IO.Error → String -| unexpectedEof => "End of file" +| unexpectedEof => "end of file" | inappropriateType (some fn) code details => fopenErrorToString "inappropriate type" fn code details | inappropriateType none code details => otherErrorToString "inappropriate type" code details | interrupted fn code details => fopenErrorToString "interrupted system call" fn code details diff --git a/tests/lean/file_not_found.lean.expected.out b/tests/lean/file_not_found.lean.expected.out index d90ee82c42..80f450f49e 100644 --- a/tests/lean/file_not_found.lean.expected.out +++ b/tests/lean/file_not_found.lean.expected.out @@ -3,7 +3,7 @@ file_not_found.lean:6:0: error: no such file or directory (error code: 2) file: non-existent-file.txt -file_not_found.lean:12:0: error: Permission denied (error code: 13) +file_not_found.lean:12:0: error: permission denied (error code: 13) file: readonly.txt file_not_found.lean:13:0: error: invalid argument (error code: 9, bad file descriptor)