From 7cd0e0a7a5694fce627c370fe8964ffae2cd4320 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Feb 2020 12:23:43 -0800
Subject: [PATCH] feat: make sure we can see error messages at `#check_failure`

---
 src/Init/Lean/Elab/Command.lean | 2 +-
 src/Init/Lean/Message.lean      | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 890d48fc92..c670f07203 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -533,7 +533,7 @@ let resetMessages : CommandElabM MessageLog := do {
   pure messages
 };
 let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do {
-  modify $ fun s => { messages := prevMessages ++ s.messages.eraseErrors, .. s }
+  modify $ fun s => { messages := prevMessages ++ s.messages.errorsToWarnings, .. s }
 };
 prevMessages ← resetMessages;
 succeeded ← finally (catch (do x; hasNoErrorMessages) (fun ex => pure false)) (restoreMessages prevMessages);
diff --git a/src/Init/Lean/Message.lean b/src/Init/Lean/Message.lean
index b245ea1d32..5ee4707a15 100644
--- a/src/Init/Lean/Message.lean
+++ b/src/Init/Lean/Message.lean
@@ -166,8 +166,8 @@ log.msgs.any $ fun m => match m.severity with
 | MessageSeverity.error => true
 | _                     => false
 
-def eraseErrors (log : MessageLog) : MessageLog :=
-{ msgs := log.msgs.foldl (fun r m => match m.severity with | MessageSeverity.error => r | _ => r.push m) {} }
+def errorsToWarnings (log : MessageLog) : MessageLog :=
+{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { severity := MessageSeverity.warning, .. m} | _ => m) }
 
 def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
 log.msgs.forM f