From 5f41cc71ffd489822989693bb7ff3d235408d838 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 13 Jan 2025 11:36:01 +0100 Subject: [PATCH] fix: trace indentation in info view (#6597) 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 --- src/Lean/Widget/InteractiveDiagnostic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 4b137e04590b..2ad00405d149 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -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}⟩