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

Makarius makarius at sketis.net
Sat Mar 7 14:06:02 CET 2026


On 07/03/2026 01:51, Andreas Kurz via isabelle-dev wrote:
> 
> 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 have attached the patch to fix this issue to this email.

Again the ugly word "to fix". I've inspected your change wrt. the history, and 
found this spot where I introduced the potential problem:

changeset:   83555:b2857541a531
user:        wenzelm
date:        Fri Nov 14 22:18:37 2025 +0100
files:       src/Tools/VSCode/src/lsp.scala 
src/Tools/VSCode/src/pretty_text_panel.scala 
src/Tools/VSCode/src/vscode_rendering.scala
description:
clarified signature: more explicit types;
minor performance tuning: postpone ("text_" + colot.toString) after filtering 
and grouping;
misc tuning;


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


	Makarius



More information about the isabelle-dev mailing list