[PATCH] VSCode fix: Dynamic_Ouput JSON serialization error `Bad JSON value: isabelle.vscode.LSP$$$Lambda`

[Andreas Kurz]

>> 
>> While testing the Isabelle2025-2 with the VSCode Language Server, I 
>> encountered a crash in the Dynamic_Output session consumer. The error 
>> reported in the LSP logs is:
>> 
>> [ERROR] "rpc" "isabelle" "stderr" '*** Session consumer failure: 
>> "isabelle.vscode.Dynamic_Output"\n*** Bad JSON value: 
>> isabelle.vscode.LSP$$ $Lambda/...\n'
> 
> Thanks for the hint. How did you get this problem? I could not guess on 
> the spot how to trigger it.
> 
> It is mandatory to have a reproducible error situation, before applying 
> any "fixes" blindy.

I worded this actually very badly. I tested it in Neovim with a plugin 
and recieved this above error. I later tried running VSCode to check if 
the LSP is still working there.
I ran the VSCode Extension now and there everything seemed to work with 
no issues even with this serialization bug. But why?

Server start command for VSCode: `isabelle vscode_server -l HOL -o 
show_results=false`
Server start command for Neovim: `isabelle vscode_server -o 
vscode_pide_extensions -o vscode_html_output=false -o 
editor_output_state`

> So to *amend* that properly, I need a reproducible error situation, and 
> then do a change that relates to b2857541a531.

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`

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.

      Andreas