From bf643106031c34d4db40aabee4a436c5e496abb8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Jul 2019 07:21:24 -0700
Subject: [PATCH] chore(library/init/lean): minor

---
 library/init/lean/message.lean       | 16 +++++++++-------
 library/init/lean/parser/parser.lean |  3 ++-
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean
index cd6c5c05cd..099866b8e4 100644
--- a/library/init/lean/message.lean
+++ b/library/init/lean/message.lean
@@ -9,6 +9,9 @@ prelude
 import init.data.tostring init.lean.position
 
 namespace Lean
+def mkErrorStringWithPos (filename : String) (line col : Nat) (msg : String) : String :=
+filename ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg
+
 inductive MessageSeverity
 | information | warning | error
 
@@ -23,13 +26,12 @@ structure Message :=
 
 namespace Message
 protected def toString (msg : Message) : String :=
-msg.filename ++ ":" ++ toString msg.pos.line ++ ":" ++ toString msg.pos.column ++ ": " ++
-(match msg.severity with
- | MessageSeverity.information => ""
- | MessageSeverity.warning => "warning: "
- | MessageSeverity.error => "error: ") ++
-(if msg.caption == "" then "" else msg.caption ++ ":\n") ++
-msg.text
+mkErrorStringWithPos msg.filename msg.pos.line msg.pos.column
+ ((match msg.severity with
+   | MessageSeverity.information => ""
+   | MessageSeverity.warning => "warning: "
+   | MessageSeverity.error => "error: ") ++
+  (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ msg.text)
 
 instance : Inhabited Message :=
 ⟨{ filename := "", pos := ⟨0, 1⟩, text := ""}⟩
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 164397264e..295d687bc0 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -7,6 +7,7 @@ prelude
 import init.lean.position
 import init.lean.syntax
 import init.lean.toexpr
+import init.lean.message
 import init.lean.environment
 import init.lean.attributes
 import init.lean.parser.trie
@@ -146,7 +147,7 @@ match s.errorMsg with
 | none     => ""
 | some msg =>
   let pos := ctx.fileMap.toPosition s.pos;
-  ctx.filename ++ ":" ++ toString pos.line ++ ":" ++ toString pos.column ++ " " ++ toString msg
+  mkErrorStringWithPos ctx.filename pos.line pos.column (toString msg)
 
 def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState :=
 match s with