Problems with unsupported Isabelle/PIDE editors

[Makarius]

On 09/03/2026 16:17, Andreas Kurz wrote:
> 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.

I've looked through this briefly. Thomas Lindae boldly claims "This plugin 
requires changeset aa77be3e8329 or later of Isabelle to work." as if there 
would be a global principle of monotonicity on the changeset history, without 
any precautions to actually get there.

I will not give a lecture on proper software design and maintenance. Instead, 
I have now produced this change:

changeset:   84196:f9bed2fc64c8
tag:         tip
user:        wenzelm
date:        Mon Mar 09 16:40:21 2026 +0100
files:       src/Tools/VSCode/src/lsp.scala 
src/Tools/VSCode/src/vscode_resources.scala
description:
recover json_entries from b2857541a531: required for unproven Neovim 
experiments, see also isabelle.vscode.Pretty_Text_Panel with 
vscode_html_output=false;
renamed "json" to "notification", to emphasize its semantics;


That does not mean that the Neovim experiment will still work for the next 
Isabelle release, it can easily break again the way it has been done. Someone 
who cares about it needs to actively support its case within the specified 
time window: https://sketis.net/2025/plan-for-isabelle2026-october-2026


 > If you plan to create a general LSP that works for editors outside of VSCode
 > then a JSON protocol would be prefered.

We don't plan that, because LSP, despite its popularity, needs to be counted 
as a failure. It covers too few aspects of what is really required. And the 
JSON wrapping for the protocol messages is a performance bottle-neck.

Whenever we redo Isabelle/VSCode seriously, there will be a more direct, 
non-JSON protocol.


	Makarius