Skip to content

fix: trace indentation in info view#6597

Merged
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-qmkoplkkqzpx
Jan 13, 2025
Merged

fix: trace indentation in info view#6597
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-qmkoplkkqzpx

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Jan 10, 2025

This PR fixes the indentation of nested traces nodes in the info view.

image

Fixes #6389

@Kha Kha requested a review from mhuisi January 10, 2025 13:30
@Kha Kha requested a review from Vtec234 as a code owner January 10, 2025 13:30
@Kha Kha force-pushed the push-qmkoplkkqzpx branch from b5b0531 to 0d7a0dc Compare January 10, 2025 13:34
Kha
Kha commented Jan 10, 2025
View reviewed changes
src/Lean/Widget/InteractiveDiagnostic.lean
| .widget wi alt =>
return .tag (.widget wi (← fmtToTT alt col)) default
| .trace cls msg collapsed children => do
let col := col + tt.stripTags.length - 2
Copy link
Copy Markdown
Member Author

@Kha Kha Jan 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe tt.stripTags.length used to be always 2 until it became always 0 in ec59e7a#diff-c247a7de43e5ee7af1aff908c4d8e11a00d2c175a1892bf8a485c5b69450a331L162-R178

@Kha Kha added the changelog-server Language server, widgets, and IDE extensions label Jan 10, 2025
@Kha
Copy link
Copy Markdown
Member Author

Kha commented Jan 10, 2025 •
edited
Loading

Notes:

  • The existing code is hard to understand and not commented so my certainty in the change is not very high. On the other hand, we don't really use traces in very heterogeneous contexts so if the above one looks fine, we're probably good.
  • Apart from the regression noted above, there is likely a change to more lazy nodes that created this issue in the first place

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 10, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jan 10, 2025
Update lean-toolchain for testing leanprover/lean4#6597
9e1da85
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 10, 2025
Update lean-toolchain for testing leanprover/lean4#6597
ee53b2b
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 10, 2025
@ghost
Copy link
Copy Markdown

ghost commented Jan 10, 2025

Mathlib CI status (docs):

@Kha Kha added this pull request to the merge queue Jan 13, 2025
Merged via the queue into leanprover:master with commit 5f41cc7 Jan 13, 2025
@Kha Kha deleted the push-qmkoplkkqzpx branch January 14, 2025 10:49
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@Kha @luisacicolini
fix: trace indentation in info view (leanprover#6597)
15faf4e 
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 leanprover#6389
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@Kha @JovanGerb
fix: trace indentation in info view (leanprover#6597)
fb66358 
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 leanprover#6389
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mhuisi mhuisi mhuisi approved these changes

@Vtec234 Vtec234 Awaiting requested review from Vtec234 Vtec234 is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Trace nodes do not nest correctly in the infoview

2 participants

@Kha @mhuisi