lsp: added decoration_request notification;

--- a/src/Tools/VSCode/src/language_server.scala	Thu May 16 11:59:33 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon May 27 13:17:09 2024 +0200
@@ -232,6 +232,12 @@
     }
 
 
+  /* decoration request */
+
+  private def decoration_request(file: JFile): Unit =
+    resources.force_decorations(channel, file)
+
+
   /* init and exit */
 
   def init(id: LSP.Id): Unit = {
@@ -448,6 +454,7 @@
           case LSP.Hover(id, node_pos) => hover(id, node_pos)
           case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
+          case LSP.Decoration_Request(file) => decoration_request(file)
           case LSP.Caret_Update(caret) => update_caret(caret)
           case LSP.Output_Set_Margin(margin) => dynamic_output.set_margin(margin)
           case LSP.State_Init(id) => State_Panel.init(id, server)

--- a/src/Tools/VSCode/src/lsp.scala	Thu May 16 11:59:33 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Mon May 27 13:17:09 2024 +0200
@@ -489,6 +489,18 @@
           ))
       )
   }
+  
+  object Decoration_Request {
+    def unapply(json: JSON.T): Option[JFile] =
+      json match {
+        case Notification("PIDE/decoration_request", Some(params)) =>
+          for {
+            uri <- JSON.string(params, "uri")
+            if Url.is_wellformed_file(uri)
+          } yield Url.absolute_file(uri)
+        case _ => None
+      }
+  }
 
 
   /* caret update: bidirectional */

--- a/src/Tools/VSCode/src/vscode_model.scala	Thu May 16 11:59:33 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon May 27 13:17:09 2024 +0200
@@ -205,11 +205,8 @@
   def publish(
     rendering: VSCode_Rendering
   ): (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = {
-    val diagnostics = rendering.diagnostics
-    val decorations =
-      if (node_visible) rendering.decorations
-      else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) }
-
+    val (diagnostics, decorations, model) = publish_full(rendering)
+    
     val changed_diagnostics =
       if (diagnostics == published_diagnostics) None else Some(diagnostics)
     val changed_decorations =
@@ -217,7 +214,18 @@
       else if (published_decorations.isEmpty) Some(decorations)
       else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
 
-    (changed_diagnostics, changed_decorations,
+    (changed_diagnostics, changed_decorations, model)
+  }
+
+  def publish_full(
+    rendering: VSCode_Rendering
+  ): (List[Text.Info[Command.Results]],List[VSCode_Model.Decoration], VSCode_Model) = {
+    val diagnostics = rendering.diagnostics
+    val decorations =
+      if (node_visible) rendering.decorations
+      else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) }
+
+    (diagnostics, decorations,
       copy(published_diagnostics = diagnostics, published_decorations = decorations))
   }
 

--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu May 16 11:59:33 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon May 27 13:17:09 2024 +0200
@@ -360,6 +360,19 @@
   }
 
 
+  /* decoration requests */
+
+  def force_decorations(channel: Channel, file: JFile): Unit = {
+    val model = state.value.models(file)
+    val rendering1 = rendering(model)
+    val (_, decos, model1) = model.publish_full(rendering1)
+    if (pide_extensions) {
+      channel.write(rendering1.decoration_output(decos).json(file))
+    }
+  }
+
+
+
   /* spell checker */
 
   val spell_checker = new Spell_Checker_Variable