src/Tools/VSCode/src/dynamic_output.scala

--- a/src/Tools/VSCode/src/dynamic_output.scala	Sun Jun 30 15:32:12 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sun Jun 30 15:32:19 2024 +0200
@@ -58,7 +58,7 @@
     pretty_panel_.change(p => Some(Pretty_Text_Panel(
       server.resources,
       server.channel,
-      (output_text, decorations) => { server.channel.write(LSP.Dynamic_Output(output_text, decorations)) }
+      LSP.Dynamic_Output.apply,
     )))
     handle_update(None)
   }