From 36fbf53a7996f2863df9640d592ddb14de3f08d8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Oct 2022 10:31:14 +0200
Subject: [PATCH] chore: improve trace.Elab.info formatting

---
 src/Lean/Elab/InfoTree/Main.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index f7133b30a2..78fe213446 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -84,10 +84,11 @@ private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format :=
   let endPos := stx.getTailPos?.getD pos
   f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}"
 where fmtPos pos info :=
-    let pos := format <| ctx.fileMap.toPosition pos
-    match info with
-    | SourceInfo.original ..  => pos
-    | _                       => f!"{pos}†"
+  let pos := format <| ctx.fileMap.toPosition pos
+  match info with
+  | .original ..                      => pos
+  | .synthetic (canonical := true) .. => f!"{pos}†!"
+  | _                                 => f!"{pos}†"
 
 private def formatElabInfo (ctx : ContextInfo) (info : ElabInfo) : Format :=
   if info.elaborator.isAnonymous then