lsp: added Output_Set_Margin and State_Set_Margin Notifications;

--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 01 18:48:26 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Thu May 09 22:22:44 2024 +0200
@@ -18,6 +18,7 @@
       restriction: Option[Set[Command]],
       html_output: Boolean,
       margin: Double,
+      force: Boolean,
     ): State = {
       val st1 =
         resources.get_caret() match {
@@ -37,7 +38,7 @@
             }
             else this
         }
-      if (st1.output != output) {
+      if (st1.output != output || force) {
         if (html_output) {
           val node_context =
             new Browser_Info.Node_Context {
@@ -68,11 +69,11 @@
 
 class Dynamic_Output private(server: Language_Server) {
   private val state = Synchronized(Dynamic_Output.State())
-  private val margin: Double = 80
+  private var margin: Double = 80
 
-  private def handle_update(restriction: Option[Set[Command]]): Unit = {
+  private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
     val html_output = server.resources.html_output
-    state.change(_.handle_update(server.resources, server.channel, restriction, html_output, margin))
+    state.change(_.handle_update(server.resources, server.channel, restriction, html_output, margin, force))
   }
 
 
@@ -97,4 +98,9 @@
     server.session.commands_changed -= main
     server.session.caret_focus -= main
   }
+
+  def set_margin(margin: Double): Unit = {
+    this.margin = margin
+    handle_update(None, force = true)
+  }
 }

--- a/src/Tools/VSCode/src/language_server.scala	Mon Jul 01 18:48:26 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Thu May 09 22:22:44 2024 +0200
@@ -441,11 +441,13 @@
           case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
           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)
           case LSP.State_Exit(state_id) => State_Panel.exit(state_id)
           case LSP.State_Locate(state_id) => State_Panel.locate(state_id)
           case LSP.State_Update(state_id) => State_Panel.update(state_id)
           case LSP.State_Auto_Update(state_id, enabled) => State_Panel.auto_update(state_id, enabled)
+          case LSP.State_Set_Margin(state_id, margin) => State_Panel.set_margin(state_id, margin)
           case LSP.Preview_Request(file, column) => request_preview(file, column)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }

--- a/src/Tools/VSCode/src/lsp.scala	Mon Jul 01 18:48:26 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Thu May 09 22:22:44 2024 +0200
@@ -524,6 +524,17 @@
       Notification("PIDE/dynamic_output", JSON.Object("content" -> content))
   }
 
+  object Output_Set_Margin {
+    def unapply(json: JSON.T): Option[Double] =
+      json match {
+        case Notification("PIDE/output_set_margin", Some(params)) =>
+          for {
+            margin <- JSON.double(params, "margin")
+          } yield (margin)
+        case _ => None
+      }
+  }
+
 
   /* state output */
 
@@ -562,6 +573,18 @@
       }
   }
 
+  object State_Set_Margin {
+    def unapply(json: JSON.T): Option[(Counter.ID, Double)] =
+      json match {
+        case Notification("PIDE/state_set_margin", Some(params)) =>
+          for {
+            id <- JSON.long(params, "id")
+            margin <- JSON.double(params, "margin")
+          } yield (id, margin)
+        case _ => None
+      }
+  }
+
 
   /* preview */
 

--- a/src/Tools/VSCode/src/state_panel.scala	Mon Jul 01 18:48:26 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Thu May 09 22:22:44 2024 +0200
@@ -40,6 +40,12 @@
   def auto_update(id: Counter.ID, enabled: Boolean): Unit =
     instances.value.get(id).foreach(state =>
       state.server.editor.send_dispatcher(state.auto_update(Some(enabled))))
+
+  def set_margin(id: Counter.ID, margin: Double): Unit =
+    instances.value.get(id).foreach(state => {
+      state.margin = margin
+      state.server.editor.send_dispatcher(state.update())
+    })
 }
 
 
@@ -47,7 +53,7 @@
   /* output */
 
   val id: Counter.ID = State_Panel.make_id()
-  private val margin: Double = 80
+  var margin: Double = 80
 
   private def output(content: String): Unit =
     server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))