# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715784879 -7200
# Node ID 9c5a4ba4ced6c26fc99f58feee0642347eb6fb4d
# Parent  07ed4ce5c6c99025b7c7e49bec90ac8d37cd57d9
lsp: unified PIDE/decorations and dynamic output decorations format;

diff -r 07ed4ce5c6c9 -r 9c5a4ba4ced6 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Wed May 15 00:11:34 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed May 15 16:54:39 2024 +0200
@@ -71,6 +71,7 @@
               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
 
           channel.write(LSP.Dynamic_Output(output, Some(decorations)))
         }
diff -r 07ed4ce5c6c9 -r 9c5a4ba4ced6 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Wed May 15 00:11:34 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Wed May 15 16:54:39 2024 +0200
@@ -520,14 +520,14 @@
   /* dynamic output */
 
   object Dynamic_Output {
-    def apply(content: String, decorations: Option[List[(Line.Range, String)]] = None): JSON.T =
+    def apply(content: String, decorations: Option[List[(String, List[Decoration_Options])]] = 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)
+              "type" -> decoration._1,
+              "content" -> decoration._2.map(_.json))
             ))
         ))
   }