max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: improve trace.Elab.info formatting

Browse source
This commit is contained in:
Sebastian Ullrich 2022-10-19 10:31:14 +02:00
parent e55badef05
commit 36fbf53a79
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/InfoTree/Main.lean
View file

@ -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