feat: store endPos at Log.lean

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 :=

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