# HG changeset patch
# User wenzelm
# Date 1753730251 -7200
# Node ID 77a3d85592880fa39bb159638deda208b3f8a598
# Parent  90e4e90915319cc07820901e5215e93825816e9a
tuned signature;
omit obsolete "force", following 2ca0c01164cd;

diff -r 90e4e9091531 -r 77a3d8559288 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 21:13:09 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 21:17:31 2025 +0200
@@ -19,7 +19,7 @@
   def pretty_panel: Pretty_Text_Panel =
     pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
 
-  private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
+  private def handle_update(restriction: Option[Set[Command]] = None): Unit = {
     val output =
       server.resources.get_caret() match {
         case None => Editor.Output.init
@@ -36,10 +36,10 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case changed: Session.Commands_Changed =>
-        handle_update(if (changed.assignment) None else Some(changed.commands))
+        handle_update(restriction = if (changed.assignment) None else Some(changed.commands))
 
       case Session.Caret_Focus =>
-        handle_update(None)
+        handle_update()
     }
 
   def init(): Unit = {
@@ -50,7 +50,7 @@
         server.session,
         server.channel,
         LSP.Dynamic_Output.apply)))
-    handle_update(None)
+    handle_update()
   }
 
   def exit(): Unit = {