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

chore: getMessageStringEx: show exception

Browse source
This commit is contained in:
Sebastian Ullrich 2020-09-17 13:51:02 +02:00 • committed by Leonardo de Moura
parent 6a91fb1613
commit f4e6635f2b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Message.lean
View file

@ -172,8 +172,8 @@ instance : Inhabited Message :=
@[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
@[export lean_message_string] unsafe def getMessageStringEx (msg : Message) : String :=
match unsafeIO (msg.data.toString) with -- hack: this is going to be deleted
| Except.ok msg => msg
| _ => "error"
| Except.ok msg => msg
| Except.error e => "error formatting message: " ++ toString e
end Message