# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715853605 -7200
# Node ID f1aef71103296af14ce35d8a8189cea90f182e9d
# Parent  23fa5e6d8a86e6e69bfb0330c57f11053d238669
lsp: added decorations to dynamic output;

diff -r 23fa5e6d8a86 -r f1aef7110329 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Thu May 09 22:24:19 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Thu May 16 12:00:05 2024 +0200
@@ -56,8 +56,23 @@
           val html = node_context.make_html(elements, formatted)
           channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
         } else {
-          val output = resources.output_pretty(Pretty.separate(st1.output), margin = margin)
-          channel.write(LSP.Dynamic_Output(output))
+          val separate = Pretty.separate(st1.output)
+          val formatted = Pretty.formatted(separate, margin = margin)
+          val tree = Markup_Tree.from_XML(formatted)
+
+          val output = resources.output_pretty(separate, margin = margin)
+
+          val document = Line.Document(output)
+          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))
+            })
+
+          channel.write(LSP.Dynamic_Output(output, Some(decorations)))
         }
       }
       st1
diff -r 23fa5e6d8a86 -r f1aef7110329 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu May 09 22:24:19 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Thu May 16 12:00:05 2024 +0200
@@ -520,8 +520,16 @@
   /* dynamic output */
 
   object Dynamic_Output {
-    def apply(content: String): JSON.T =
-      Notification("PIDE/dynamic_output", JSON.Object("content" -> content))
+    def apply(content: String, decorations: Option[List[(Line.Range, String)]] = None): JSON.T =
+      Notification("PIDE/dynamic_output",
+        JSON.Object("content" -> content) ++
+        JSON.optional(
+          "decorations" -> decorations.map(decorations =>
+            decorations.map(decoration => JSON.Object(
+              "range" -> Range.compact(decoration._1),
+              "type" -> decoration._2)
+            ))
+        ))
   }
 
   object Output_Set_Margin {