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

chore: cleanup Message.toString

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-12 09:57:46 -08:00
parent 74c2d1dca9
commit 9f7435b5be
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Message.lean
View file

@ -151,13 +151,12 @@ namespace Message
protected def toString (msg : Message) : IO String := do
let mut str ← msg.data.toString
str :=
(match msg.severity with
| MessageSeverity.information => ""
| MessageSeverity.warning => mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column "warning: "
| MessageSeverity.error => mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column "error: ") ++
(if msg.caption == "" then "" else msg.caption ++ ":\n") ++
str
unless msg.caption == "" do
str := msg.caption ++ ":\n" ++ str
match msg.severity with
| MessageSeverity.information => pure ()
| MessageSeverity.warning => str := mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column "warning: " ++ str
| MessageSeverity.error => str := mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column "error: " ++ str
if str.isEmpty || str.back != '\n' then
str := str ++ "\n"
return str