chore(library/init/lean): minor

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 := ""}⟩

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