Problems with unsupported Isabelle/PIDE editors

[Makarius]

[This thread has a new subject to capture the true situation better.]

On 08/03/2026 00:07, Andreas Kurz wrote:
> 
> To reproduce this issue in VSCode you have to set `vscode_html_output=false` 
> in settings.
> [Info  - 11:54:53 PM] Welcome to Isabelle/HOL (Isabelle2025-2)
> *** Session consumer failure: "isabelle.vscode.Dynamic_Output"
> *** Bad JSON value: isabelle.vscode.LSP$$$Lambda/0x00007ff0244844c0 at 38e3ab38
> 
> Then I get the same error as I do in Neovim.
> 
> I also have a good guess why it does fail with html_output=false, but not with 
> html_output=true.
> In file `src/Tools/VSCode/src/pretty_text_panel.scala`
> - if html_output is true it calls `json_output(HTML.source(html).toString, 
> None)` (line 60), the decorations parameter is None it will not include the 
> "decorations" key in json.
> - if html_output is false it calls `json_output(converted_text, 
> Some(LSP.Decoration(entries)))` (line 81), the decorations are not None and 
> therefore they are serialized to a eta expansion.
> where json_output is set to `LSP.Dynamic_Output.apply` in `src/Tools/VSCode/ 
> src/dynamic_output.scala:49`

That is really bad. The deeper problem is that the author, Thomas Lindae, has 
made variants of the Isabelle/LSP implementation, specifically for his private 
Neovim experiments. The details, and expectations of the other side, are left 
implicit, though.

So we have an unmaintainable situations, or "bogs" instead of "bugs".


> 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?

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.


	Makarius