# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715853573 -7200
# Node ID f1e0ca5aaa6bb38f8f8c6e50518883aec17f964a
# Parent  b659316593648a7ba8138d11976afd584436dd6a
lsp: added decorations to state updates;

diff -r b65931659364 -r f1e0ca5aaa6b src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu May 16 11:59:06 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Thu May 16 11:59:33 2024 +0200
@@ -545,9 +545,21 @@
   /* state output */
 
   object State_Output {
-    def apply(id: Counter.ID, content: String, auto_update: Boolean): JSON.T =
+    def apply(
+       id: Counter.ID,
+       content: String,
+       auto_update: Boolean,
+       decorations: Option[List[(String, List[Decoration_Options])]] = None
+    ): JSON.T =
       Notification("PIDE/state_output",
-        JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update))
+        JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++
+        JSON.optional(
+          "decorations" -> decorations.map(decorations =>
+            decorations.map(decoration => JSON.Object(
+              "type" -> decoration._1,
+              "content" -> decoration._2.map(_.json))
+            ))
+        ))
   }
 
   class State_Id_Notification(name: String) {
diff -r b65931659364 -r f1e0ca5aaa6b src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Thu May 16 11:59:06 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Thu May 16 11:59:33 2024 +0200
@@ -44,7 +44,7 @@
   def set_margin(id: Counter.ID, margin: Double): Unit =
     instances.value.get(id).foreach(state => {
       state.margin.change(_ => margin)
-      state.server.editor.send_dispatcher(state.update(force = true))
+      state.delay_margin.invoke()
     })
 }
 
@@ -55,8 +55,14 @@
   val id: Counter.ID = State_Panel.make_id()
   private val margin: Synchronized[Double] = Synchronized(server.resources.message_margin)
 
-  private def output(content: String): Unit =
-    server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
+  private val delay_margin = Delay.last(server.resources.output_delay, server.channel.Error_Logger) {
+    server.editor.send_dispatcher(update(force = true))
+  }
+
+  private def output(
+      content: String,
+      decorations: Option[List[(String, List[LSP.Decoration_Options])]] = 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))
@@ -87,7 +93,31 @@
             val html = node_context.make_html(elements, formatted)
             output(HTML.source(html).toString)
           } else {
-            output(server.resources.output_pretty(Pretty.separate(body), margin.value))
+            val separate = Pretty.separate(body)
+            val formatted = Pretty.formatted(separate, margin = margin.value)
+
+            def convert_symbols(body: XML.Body): XML.Body = {
+              body.map {
+                case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
+                case XML.Text(content) => XML.Text(Symbol.output(server.resources.unicode_symbols, content))
+              }
+            }
+
+            val tree = Markup_Tree.from_XML(convert_symbols(formatted))
+            val result = server.resources.output_pretty(separate, margin = margin.value)
+
+            val document = Line.Document(result)
+            val decorations = tree
+              .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
+                Some(Some(m.info.name))
+              })
+              .flatMap(e => e._2 match {
+                case None => None
+                case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
+              })
+              .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
+
+            output(result, Some(decorations))
           }
         })