# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715853546 -7200
# Node ID b659316593648a7ba8138d11976afd584436dd6a
# Parent  d3e0d68c50d812bd286c4710f1280fa4f1d5c83f
lsp: added delay to dynamic_output updates after a set_margin;

diff -r d3e0d68c50d8 -r b65931659364 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Wed May 15 17:04:22 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Thu May 16 11:59:06 2024 +0200
@@ -96,6 +96,10 @@
   private val margin_ = Synchronized(None: Option[Double])
   def margin: Double = margin_.value.getOrElse(server.resources.message_margin)
 
+  private val delay_margin = Delay.last(server.resources.output_delay, server.channel.Error_Logger) {
+    handle_update(None, force = true)
+  }
+
   private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
     val html_output = server.resources.html_output
     state.change(
@@ -127,6 +131,6 @@
 
   def set_margin(margin: Double): Unit = {
     margin_.change(_ => Some(margin))
-    handle_update(None, force = true)
+    delay_margin.invoke()
   }
 }
diff -r d3e0d68c50d8 -r b65931659364 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed May 15 17:04:22 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu May 16 11:59:06 2024 +0200
@@ -84,6 +84,7 @@
   def html_output: Boolean = options.bool("vscode_html_output")
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
   def message_margin: Int = options.int("vscode_message_margin")
+  def output_delay: Time = options.seconds("vscode_output_delay")
 
 
   /* document node name */