lsp: refactored conversion from Decoration_List to JSON;

--- a/src/Tools/VSCode/src/lsp.scala	Sun Jun 30 15:32:19 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Jun 30 15:32:26 2024 +0200
@@ -481,14 +481,18 @@
   type Decoration_List = List[(String, List[Decoration_Options])]
 
   sealed case class Decoration(decorations: Decoration_List) {
+    def json_entries: JSON.T =
+      decorations.map(decoration => JSON.Object(
+        "type" -> decoration._1,
+        "content" -> decoration._2.map(_.json))
+      )
+
     def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
         JSON.Object(
           "uri" -> Url.print_file(file),
-          "entries" -> decorations.map(decoration => JSON.Object(
-            "type" -> decoration._1,
-            "content" -> decoration._2.map(_.json))
-          ))
+          "entries" -> json_entries
+        )
       )
   }
   
@@ -534,16 +538,11 @@
   /* dynamic output */
 
   object Dynamic_Output {
-    def apply(content: String, decorations: Option[Decoration_List] = None): JSON.T =
+    def apply(content: String, decoration: Option[Decoration] = None): JSON.T =
       Notification("PIDE/dynamic_output",
         JSON.Object("content" -> content) ++
-        JSON.optional(
-          "decorations" -> decorations.map(decorations =>
-            decorations.map(decoration => JSON.Object(
-              "type" -> decoration._1,
-              "content" -> decoration._2.map(_.json))
-            ))
-        ))
+        JSON.optional("decorations" -> decoration.map(_.json_entries))
+      )
   }
 
   object Output_Set_Margin {
@@ -563,17 +562,12 @@
        id: Counter.ID,
        content: String,
        auto_update: Boolean,
-       decorations: Option[Decoration_List] = None
+       decorations: Option[Decoration] = None
     ): JSON.T =
       Notification("PIDE/state_output",
         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))
-            ))
-        ))
+        JSON.optional("decorations" -> decorations.map(_.json_entries))
+      )
   }
 
   class State_Id_Notification(name: String) {

--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:19 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:26 2024 +0200
@@ -12,14 +12,14 @@
   def apply(
     resources: VSCode_Resources,
     channel: Channel,
-    output: (String, Option[LSP.Decoration_List]) => JSON.T
+    output: (String, Option[LSP.Decoration]) => 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]) => JSON.T
+  output: (String, Option[LSP.Decoration]) => JSON.T
 ) {
   private var current_body: XML.Body = Nil
   private var current_formatted: XML.Body = Nil
@@ -79,7 +79,7 @@
         })
         .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
 
-      val message = output(text, Some(decorations))
+      val message = output(text, Some(LSP.Decoration(decorations)))
       channel.write(message)
     }
   }