# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715286259 -7200
# Node ID 23fa5e6d8a86e6e69bfb0330c57f11053d238669
# Parent  56594fac1dabe8283d013be91c6526871d72b75d
lsp: force update after state_set_margin;

diff -r 56594fac1dab -r 23fa5e6d8a86 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Thu May 30 02:45:01 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Thu May 09 22:24:19 2024 +0200
@@ -44,7 +44,7 @@
   def set_margin(id: Counter.ID, margin: Double): Unit =
     instances.value.get(id).foreach(state => {
       state.margin.change(_ => margin)
-      state.server.editor.send_dispatcher(state.update())
+      state.server.editor.send_dispatcher(state.update(force = true))
     })
 }
 
@@ -93,12 +93,16 @@
 
   def locate(): Unit = print_state.locate_query()
 
-  def update(): Unit = {
+  def update(force: Boolean = false): Unit = {
     server.editor.current_node_snapshot(()) match {
       case Some(snapshot) =>
-        (server.editor.current_command((), snapshot), print_state.get_location) match {
-          case (Some(command1), Some(command2)) if command1.id == command2.id =>
-          case _ => print_state.apply_query(Nil)
+        if (force) {
+          print_state.apply_query(Nil)
+        } else {
+          (server.editor.current_command((), snapshot), print_state.get_location) match {
+            case (Some(command1), Some(command2)) if command1.id == command2.id =>
+            case _ => print_state.apply_query(Nil)
+          }
         }
       case None =>
     }