max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Widget
History
Sebastian Ullrich 5f41cc71ff
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
2025-01-13 10:36:01 +00:00
..
Basic.lean chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00
Diff.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
InteractiveCode.lean feat: labeled and unique sorries (#5757) 2024-12-11 23:53:02 +00:00
InteractiveDiagnostic.lean fix: trace indentation in info view (#6597) 2025-01-13 10:36:01 +00:00
InteractiveGoal.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
TaggedText.lean chore: rename Array.back to back! (#5897) 2024-10-31 09:18:18 +00:00
Types.lean feat: widget messages (#4254) 2024-05-29 06:37:42 +00:00
UserWidget.lean chore: move MessageData.ofConstName earlier (#5877) 2024-10-29 21:23:51 +00:00