# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719754339 -7200
# Node ID fb1183184e680550d401d92d285912e03efdea57
# Parent  e199c34b38e90da85c0c97145f98a67463f022ee
lsp: tuned pretty_text_panel;

diff -r e199c34b38e9 -r fb1183184e68 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)
   }
diff -r e199c34b38e9 -r fb1183184e68 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:12 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:19 2024 +0200
@@ -12,14 +12,14 @@
   def apply(
     resources: VSCode_Resources,
     channel: Channel,
-    output: (String, Option[LSP.Decoration_List]) => Unit
+    output: (String, Option[LSP.Decoration_List]) => JSON.T
   ): Pretty_Text_Panel = new Pretty_Text_Panel(resources, channel, output)
 }
 
 class Pretty_Text_Panel private(
   resources: VSCode_Resources,
   channel: Channel,
-  output: (String, Option[LSP.Decoration_List]) => Unit
+  output: (String, Option[LSP.Decoration_List]) => JSON.T
 ) {
   private var current_body: XML.Body = Nil
   private var current_formatted: XML.Body = Nil
@@ -55,7 +55,8 @@
         }
       val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
       val html = node_context.make_html(elements, formatted)
-      output(HTML.source(html).toString, None)
+      val message = output(HTML.source(html).toString, None)
+      channel.write(message)
     } else {
       def convert_symbols(body: XML.Body): XML.Body = {
         body.map {
@@ -78,7 +79,8 @@
         })
         .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
 
-      output(text, Some(decorations))
+      val message = output(text, Some(decorations))
+      channel.write(message)
     }
   }
 }
diff -r e199c34b38e9 -r fb1183184e68 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Sun Jun 30 15:32:12 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Sun Jun 30 15:32:19 2024 +0200
@@ -53,9 +53,6 @@
 
   val id: Counter.ID = State_Panel.make_id()
 
-  private def output(content: String, decorations: Option[LSP.Decoration_List] = None): Unit =
-    server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value, decorations))
-
   private def init_response(id: LSP.Id): Unit =
     server.channel.write(LSP.State_Init.reply(id, this.id))
 
@@ -66,7 +63,7 @@
   private val pretty_panel = Synchronized(Pretty_Text_Panel(
     server.resources,
     server.channel,
-    output,
+    (content, decorations) => LSP.State_Output(id, content, auto_update_enabled.value, decorations)
   ))
 
   private val print_state =