Skip to content

Commit

Permalink
fix: trace indentation in info view
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Jan 10, 2025
1 parent d2c4471 commit b5b0531
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/Lean/Widget/InteractiveDiagnostic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,9 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
| .widget wi alt =>
return .tag (.widget wi (← fmtToTT alt col)) default
| .trace cls msg collapsed children => do
let col := col + tt.stripTags.length - 2
-- absolute column = request-level indentation (e.g. from nested lazy trace request) +
-- offset inside `fmt`
let col := indent + col
let children ←
match children with
| .lazy children => pure <| .lazy ⟨{indent := col+2, children := children.map .mk}⟩
Expand Down

0 comments on commit b5b0531

Please sign in to comment.