[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