Zixuan Fan (Dec 06 2022 at 17:14): Zixuan Fan (Dec 06 2022 at 17:14):Is it possible to have a catalogue panel in the vscode extension of Isabelle, i.e. showing all lemmata, sections, etc. on the right sidebar in the JEdit.
Mathias Fleury (Dec 06 2022 at 17:50):Maybe I should try to get my patch in the isabelle repo :thinking:
Mathias Fleury (Dec 06 2022 at 17:52):The code is included in the lsp server at https://github.com/m-fleury/isabelle-emacs/ (you can just ignore the entire emacs stuff)
Mathias Fleury (Dec 06 2022 at 17:53):BTW if understands vscode enough to create a theory panel, that information is also very easy to get
Mathias Fleury (Dec 06 2022 at 17:53):I was just never motivated enough to write a plugin in VSCode to print that information
Mathias Fleury (Dec 06 2022 at 17:53):(or more precisely: it worked but was very very ugly)
Zixuan Fan (Dec 06 2022 at 18:02):I guess I can try isabelle-emacs, then. I recently learned that proof general is good is some perspectives.
Mathias Fleury (Dec 06 2022 at 18:02):Just clone the repo and run "path-to-repo/bin/isabelle vscode"
Mathias Fleury (Dec 06 2022 at 18:04):you get the completely normal vscode from isabelle (I don't touch that) there is just 1 new features in the vscode communication…
Mathias Fleury (Dec 06 2022 at 18:05):(you have to open the outline)
Mathias Fleury (Dec 06 2022 at 18:06):
Mathias Fleury (Dec 06 2022 at 18:08):(no scary emacs involved, no change in your habits)
Christian Zimmerer (Dec 13 2022 at 23:45):I would recommend to use Emacs over VScode for Isabelle so far though. The experience is way better for me. It's still a little tradeoff from the jedit interface, but you get to keep your keybindings and all convenience features from Emacs :)
Julian (Dec 14 2022 at 10:42):Hope it's not off topic but this comes to mind: https://xkcd.com/378/
Manuel Eberl (Dec 14 2022 at 13:29):In the good old days everyone wrote Isabelle in emacs! (ProofGeneral to be precise).
But back then there was official support for it. I cannot imagine how painful it must be these days…
Last updated: Dec 21 2024 at 16:20 UTC