Skip to content

Commit

Permalink
fix: trace indentation in info view (#6597)
Browse files Browse the repository at this point in the history
This PR fixes the indentation of nested traces nodes in the info view.


![image](https://github.com/user-attachments/assets/c13ac2a2-e994-4900-9201-0d86889f6a1b)

Fixes #6389
  • Loading branch information
Kha authored Jan 13, 2025
1 parent 2421f7f commit 5f41cc7
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 5f41cc7

Please sign in to comment.