Topic: Bracket Pair colours
Eric Rodriguez (Sep 29 2021 at 15:46):
I'm sure many people here use bracket pair colourisation; it's now a core VSCode feature with much improved performance (and hopefully also much improved lack of bugs!)
Eric Rodriguez (Sep 29 2021 at 15:47):
(also, the article is really interesting about how they tried to optimise the feature and its algorithmics)
Gabriel Ebner (Sep 29 2021 at 15:50):
I was surprised to see a familiar face on the article: @Henning Dieterichs also rewrote the abbreviations expander in our vscode extension.
Riccardo Brasca (Sep 29 2021 at 16:06):
And it finally works over SSH!!
Sebastian Ullrich (Sep 29 2021 at 16:33):
He's a former student of ours :) https://pp.ipd.kit.edu/publication.php?id=dieterichs21masterarbeit
Bryan Gin-ge Chen (Sep 29 2021 at 16:36):
(We should add masters theses like this to our papers page!)
Kevin Buzzard (Sep 29 2021 at 16:53):
We might want to distinguish published papers from unpublished MSc theses? Not sure. I have supervised a few MSc theses which do cool Lean stuff (e.g. define group cohomology in Lean)
Eric Rodriguez (Sep 29 2021 at 22:12):
image.png turns out this feature still has some lean-specific errors ;b (also
section ... end don't match)
Henning Dieterichs (Sep 30 2021 at 15:48):
Identifier-based bracket pairs are a known issue and will be supported soon!
Last updated: Aug 03 2023 at 10:10 UTC