From ef8c19ff7217075fee5e0e1697b5de398cddcfb9 Mon Sep 17 00:00:00 2001 From: Andreas Kurz Date: Sat, 7 Mar 2026 01:22:51 +0100 Subject: [PATCH] VSCode fix: Dynamic_Ouput JSON serialization error `Bad JSON value: isabelle.vscode.LSP$$$Lambda` --- src/Tools/VSCode/src/lsp.scala | 8 +++++--- src/Tools/VSCode/src/vscode_resources.scala | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Tools/VSCode/src/lsp.scala b/src/Tools/VSCode/src/lsp.scala index 0d15446809..3b04942415 100644 --- a/src/Tools/VSCode/src/lsp.scala +++ b/src/Tools/VSCode/src/lsp.scala @@ -552,9 +552,11 @@ object LSP { } sealed case class Decoration(entries: List[Decoration_Entry]) { - def json(file: JFile): JSON.T = + def json(file: Option[JFile]): JSON.T = Notification("PIDE/decoration", - JSON.Object("uri" -> Url.print_file(file), "entries" -> entries.map(_.json))) + JSON.Object( + "uri" -> file.map(Url.print_file(_)).orNull, + "entries" -> entries.map(_.json))) } object Decoration_Request { @@ -599,7 +601,7 @@ object LSP { def apply(content: String, decorations: Option[Decoration] = None): JSON.T = Notification("PIDE/dynamic_output", JSON.Object("content" -> content) ++ - JSON.optional("decorations" -> decorations.map(_.json))) + JSON.optional("decorations" -> decorations.map(_.json(None)))) } object Output_Set_Margin { diff --git a/src/Tools/VSCode/src/vscode_resources.scala b/src/Tools/VSCode/src/vscode_resources.scala index cb11ed0619..6048fa0614 100644 --- a/src/Tools/VSCode/src/vscode_resources.scala +++ b/src/Tools/VSCode/src/vscode_resources.scala @@ -316,7 +316,7 @@ extends Resources(session_background, log = log) { channel.write(LSP.PublishDiagnostics(file, rendering.diagnostics_output(diags))) if (pide_extensions) { for (decos <- changed_decos) - channel.write(rendering.decoration_output(decos).json(file)) + channel.write(rendering.decoration_output(decos).json(Some(file))) } (file, model1) } @@ -369,7 +369,7 @@ extends Resources(session_background, log = log) { val rendering1 = rendering(model) val (_, decos, model1) = model.publish_full(rendering1) if (pide_extensions) { - channel.write(rendering1.decoration_output(decos).json(file)) + channel.write(rendering1.decoration_output(decos).json(Some(file))) } } -- 2.52.0