From b94c5c181cfabe0285708aa4e6afa4a3f94407a2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 20 Jan 2021 18:40:25 +0100
Subject: [PATCH] chore: annotate syntheticness in info format

---
 src/Lean/Elab/InfoTree.lean | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index f268c2a9ec..72b4bed239 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -108,17 +108,23 @@ def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPConte
 def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
   ppTerm (info.toPPContext lctx) stx
 
+private def formatStxRange (cinfo : ContextInfo) (stx : Syntax) : Format := do
+  let pos    := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD pos
+  return f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}"
+where fmtPos pos info :=
+    let pos := format <| cinfo.fileMap.toPosition pos
+    match info with
+    | SourceInfo.original ..  => pos
+    | _                       => f!"{pos}†"
+
 def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do
   cinfo.runMetaM info.lctx do
-    let pos    := info.stx.getPos?.getD 0
-    let endPos := info.stx.getTailPos?.getD pos
-    return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
+    return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange cinfo info.stx}"
 
 def FieldInfo.format (cinfo : ContextInfo) (info : FieldInfo) : IO Format := do
   cinfo.runMetaM info.lctx do
-    let pos    := info.stx.getPos?.getD 0
-    let endPos := info.stx.getTailPos?.getD pos
-    return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
+    return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange cinfo info.stx}"
 
 def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format :=
   if goals.isEmpty then