From 1ff7950a779d85935fecadd880596f177e96a975 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jan 2020 16:19:07 -0800
Subject: [PATCH] feat: use `truncateTrailing` at error messages

---
 src/Init/Lean/Elab/Util.lean | 2 +-
 src/Init/Lean/Syntax.lean    | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index d4bdbf5a45..6739cc4b7c 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/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
 
diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 46263d0f4d..2d6ff22b63 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/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.