Problems with unsupported Isabelle/PIDE editors

[Andreas Kurz]

On 2026-03-09 13:46, Makarius wrote:
>> While I know Neovim falls outside the officially supported 
>> environments, this bug affects the LSP servers JSON serialization 
>> under certain configurations, so it would be great if this could be 
>> addressed.
> 
> Can you point to the relevant Neovim sources, presumably also by Thomas 
> Lindae?

So the Neovim plugin that I use is this one: 
https://github.com/Treeniks/isabelle-lsp.nvim
The initialization of the server or rather the definition of the command 
is done here: 
https://github.com/Treeniks/isabelle-lsp.nvim/blob/master/lua/utils.lua#L9
ofcourse with the option `vscode_html_output=false` set to false, then 
rendering the content directly with the decorations in the terminal.


> We need explicit proof that it is worth keeping it for now, and not 
> remove the bad code paths in Isabelle/LSP, to avoid such problems.
> 
> Note that Isabelle has this principle of "garbage collection on 
> sources" for unused/unmaintained material.

This makes total sense, reduce the complexity and simplify to the actual 
needed things.
If you plan to create a general LSP that works for editors outside of 
VSCode then a JSON protocol would be prefered. (I see that this is a big 
undertaking for a (currently) small reward.)