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

[Andreas Kurz]

Hello,

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'

Problem:
In isabelle.vscode.LSP.Dynamic_Output, the decorations field is 
constructed using decorations.map(_.json). In the current Scala 
environment, this appears to trigger an unintended eta-expansion, 
because of the definition of Decoration.json(file: JFile). Passing a 
lambda function to the JSON serializer rather than evaluating the 
underlying data. This results in an error where the Output window would 
never be filled.

Fix:
Make the file input in the Decoration Optional and pass a None in case 
of the Dynamic_Ouput which will then evaluate to a json null inside of 
Decoration.json.
The other use locations of Decoration.json got changed to pass 
Some(file).

I have attached the patch to fix this issue to this email.

Kind regards,
Andreas Kurz
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle_lsp_json_fix.patch
Type: text/x-diff
Size: 2542 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260307/f80ff806/attachment.patch>