lean4-mode icon indicating copy to clipboard operation
lean4-mode copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Fix magit-section usage so the expand/contract functionality works

Open bustercopley opened this issue 11 months ago • 4 comments

Use named sections so magit-section can track which sections are expanded. Don't use sections for individual diagnostics, since they can't be tracked. Capture data in lexicals for deferred rendering by magit-insert-section-body. Use with-current-buffer (delete lean4-with-info-output-to-buffer). Make the diagnostic line:col headers into text buttons.

bustercopley avatar Mar 02 '24 01:03 bustercopley

force-push: rebase onto #51

bustercopley avatar Mar 02 '24 12:03 bustercopley

Rebased onto leanprover-community:master

bustercopley avatar Mar 06 '24 15:03 bustercopley

Can someone merge this please?

sebeaumont avatar Aug 15 '24 10:08 sebeaumont

I see no reason not to. It's just a minor bugfix. @sebeaumont, please ping Yury (@urkud) on Zulip.

bustercopley avatar Aug 15 '24 20:08 bustercopley