lsp: made margins synchronized;

--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri May 03 20:13:48 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sun Jun 30 15:29:44 2024 +0200
@@ -70,11 +70,13 @@
 
 class Dynamic_Output private(server: Language_Server) {
   private val state = Synchronized(Dynamic_Output.State())
-  private var margin: Double = 80
+  private val margin_ = Synchronized(None: Option[Double])
+  def margin: Double = margin_.value.getOrElse(server.resources.message_margin)
 
   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, force))
+    state.change(
+      _.handle_update(server.resources, server.channel, restriction, html_output, margin, force))
   }
 
 
@@ -101,7 +103,7 @@
   }
 
   def set_margin(margin: Double): Unit = {
-    this.margin = margin
+    margin_.change(_ => Some(margin))
     handle_update(None, force = true)
   }
 }

--- a/src/Tools/VSCode/src/state_panel.scala	Fri May 03 20:13:48 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Sun Jun 30 15:29:44 2024 +0200
@@ -43,7 +43,7 @@
 
   def set_margin(id: Counter.ID, margin: Double): Unit =
     instances.value.get(id).foreach(state => {
-      state.margin = margin
+      state.margin.change(_ => margin)
       state.server.editor.send_dispatcher(state.update())
     })
 }
@@ -53,7 +53,7 @@
   /* output */
 
   val id: Counter.ID = State_Panel.make_id()
-  var margin: Double = 80
+  private val margin: Synchronized[Double] = Synchronized(server.resources.message_margin)
 
   private def output(content: String): Unit =
     server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
@@ -83,11 +83,11 @@
               }
             val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
             val separate = Pretty.separate(body)
-            val formatted = Pretty.formatted(separate, margin = margin)
+            val formatted = Pretty.formatted(separate, margin = margin.value)
             val html = node_context.make_html(elements, formatted)
             output(HTML.source(html).toString)
           } else {
-            output(server.resources.output_pretty(Pretty.separate(body), margin))
+            output(server.resources.output_pretty(Pretty.separate(body), margin.value))
           }
         })