max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make sure we can see error messages at #check_failure

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-12 12:23:43 -08:00
parent 98c925ed7e
commit 7cd0e0a7a5
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Command.lean
View file

@ -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);

4
src/Init/Lean/Message.lean
View file

@ -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