Email Gateway (Apr 04 2026 at 10:40): Email Gateway (Apr 04 2026 at 10:40):From: Petteri Raita <petteri.r.raita@gmail.com>
Hey Team,
I encountered an issue with Isabelle's VSCode LSP output where decorations
fail to render and produce runtime errors.
Environment:
Observed error:
*** Session consumer failure: "isabelle.vscode.Dynamic_Output"
*** Bad JSON value: isabelle.vscode.LSP$$$Lambda/...
This suggests that a function (lambda) is being passed into the JSON layer
instead of a concrete JSON value.
The issue appears to originate from:
Tools/VSCode/src/lsp.scala
Specifically:
Before:
"entries" -> entries.map(_.json)
After:
"entries" -> json
with:
def json: JSON.T = entries.map(_.json)
The modified version resolves the issue locally and produces valid JSON,
while the original version leads to the "Bad JSON value" error above.
My interpretation is that in some contexts the original expression results
in a value that is not properly normalized into JSON.T, whereas the named
method avoids this (possibly related to eta-expansion or evaluation
context).
I am not certain if this is the correct fix or if it exposes a deeper issue
in JSON encoding or LSP interaction.
A patch (generated via git format-patch) is attached for reference.
Any feedback would be appreciated.
--
Best Regards,
Petteri Raita
+358 442592704
DTU student number 253163
s253163@student.dtu.dk
0001-Fix-decoration-JSON-encoding-for-VSCode-server-outpu.patch
Last updated: Apr 12 2026 at 02:50 UTC