feat: use truncateTrailing at error messages

src/Init/Lean/Elab/Util.lean

@@ -10,7 +10,7 @@ import Init.Lean.Parser
 namespace Lean
 
 def Syntax.prettyPrint (stx : Syntax) : Format :=
-match stx.reprint with -- TODO use syntax pretty printer
+match stx.truncateTrailing.reprint with -- TODO use syntax pretty printer
 | some str => format str.toFormat
 | none     => format stx
 

src/Init/Lean/Syntax.lean

@@ -236,6 +236,11 @@ match setTailInfoAux info stx with
 | some stx => stx
 | none     => stx
 
+def truncateTrailing (stx : Syntax) : Syntax :=
+match stx.getTailInfo with
+| none      => stx
+| some info => stx.setTailInfo info.truncateTrailing
+
 private def reprintLeaf : Option SourceInfo → String → String
 -- no source info => add gracious amounts of whitespace to definitely separate tokens
 -- Note that the proper pretty printer does not use this function.