From ccefe970dc0a54f24148ace5c5cdbca9fee416f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Dec 2020 19:09:41 -0800
Subject: [PATCH] feat: store `endPos` at `Log.lean`

---
 src/Init/Meta.lean     | 12 +++++++++++-
 src/Lean/Elab/Log.lean |  7 ++++---
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index cf38df5d3b..3d254a3de8 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -121,6 +121,12 @@ partial def getTailInfo : Syntax → Option SourceInfo
   | node _ args   => args.findSomeRev? getTailInfo
   | _             => none
 
+partial def getTailPos : Syntax → Option String.Pos
+  | atom { pos := some pos, .. }  val    => some (pos + val.bsize)
+  | ident { pos := some pos, .. } val .. => some (pos + val.toString.bsize)
+  | node _ args                          => args.findSomeRev? getTailPos
+  | _                                    => none
+
 @[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
   if i == 0 then
     none
@@ -182,7 +188,7 @@ partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
   | node k args => node k <| args.map (replaceInfo info)
   | stx         => setInfo info stx
 
-def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
+def copyHeadInfo (s : Syntax) (source : Syntax) : Syntax :=
   match source.getHeadInfo with
   | none      => s
   | some info => s.setHeadInfo info
@@ -192,6 +198,10 @@ def copyTailInfo (s : Syntax) (source : Syntax) : Syntax :=
   | none      => s
   | some info => s.setTailInfo info
 
+def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
+ let s := s.copyHeadInfo source
+ s.copyTailInfo source
+
 end Syntax
 
 def mkAtom (val : String) : Syntax :=
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index e0ee434640..1c3cb06168 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -36,11 +36,12 @@ def getRefPosition : m Position := do
 
 def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error): m Unit :=
   unless severity == MessageSeverity.error && msgData.hasSyntheticSorry do
-    let ref  := replaceRef ref (← MonadLog.getRef)
-    let pos  := ref.getPos.getD 0
+    let ref    := replaceRef ref (← MonadLog.getRef)
+    let pos    := ref.getPos.getD 0
+    let endPos := ref.getTailPos.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, data := msgData, severity := severity }
+    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
 
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
   logAt ref msgData MessageSeverity.error