change_document

[m-fleury]

I did not know you were using my Isabelle fork. I should really mention you stuff.

One question: what does your change to change_document do? If it is useful, I could just change it on my side. Or provide an option for you to avoid the patching part.

[m-fleury]

BTW once you have submitted your bachelor thesis, can you send it to me? I would be interested to read it (and if you do not manage to upstream the changes, I need to understand and merge it in my isabelle fork, I would hate to see those changes lost)

[Treeniks]

Sorry, I wanted to reach out to you ages ago anyway but laziness got the better of me. I just made the repo for the thesis public (https://github.com/Treeniks/bachelor-thesis-isabelle-vscode), you'll find the thesis as a Release.

The thesis describes the change_document change a little. Basically, the LSP intends the changes coming from the client to be applied in the order they're given and not sorted beforehand. The original commit introducing this normalization mentions something about automatic parantheses around selection, but I couldn't replicate any situation where it was needed (maybe the protocol changed since then?).

It was also the first thing I changed when I started my work on the thesis (https://github.com/Treeniks/isabelle-language-server/commit/aeeaf2f027e0505cd38c0be6bb02bec1687226fc) and I haven't found any issues with the change personally (although admittedly I don't use VSCode much).

FYI one notable change I made that's not mentioned in the thesis was to make the language server send decoration notifications for more types of decorations (https://github.com/Treeniks/isabelle-language-server/commit/dedb9efaa6597f33a4eb2ddee574eb956b12d03d). This means the language server should send decorations for keywords like theorem now. Tbh I'm not entirely sure why it was filtered in the first place.

If we manage to upstream my changes, there might be a handful of things you'll need to change for the emacs language client. The vscode_html_output option I added should also be compatible with the one your fork has, although I refactored and changed the underlying code for panels quite a bit to get formatting and highlighting working smoothly. Also the messages to inform the language server about the panel widths have changed, and State initialization is now a request instead of a notification. The vscode_unicode_symbols option was replaced by two separate vscode_symbols_edits and vscode_symbols_output options. edits is for things like auto completion, output for things like state panel content.

[m-fleury]

I read the thesis over the week-end (I liked it).

I had forgotten it, but we reached similar issues for that actually but only for vim-style editing and not consistently. But somehow it got better with emacs updates.

One more question: did you implement the symbol interface (https://github.com/m-fleury/isabelle-emacs/blob/Isabelle2024-vsce/src/Tools/VSCode/src/lsp.scala#L610C10-L610C24)? It basically is the sidekick of the LSP protocol.

I will wait to see if you manage to get your changes upstreamed. Then I will adapt my code to use your things. In particular the state/output panel changes are good but I keep them separate which VSCode did not support back then.

[Treeniks]

One more question: did you implement the symbol interface (https://github.com/m-fleury/isabelle-emacs/blob/Isabelle2024-vsce/src/Tools/VSCode/src/lsp.scala#L610C10-L610C24)? It basically is the sidekick of the LSP protocol.

no I did not. I'm not 100% sure what exactly it does though. The server implements a Hover provider, does that not give the same information?

[m-fleury]

It makes it possible to look at the structure of the theory:

That is emacs, but VScode supports it too. And here is the neovim equivalent: https://github.com/simrat39/symbols-outline.nvim.