tuned signature;
authorwenzelm
Mon, 28 Jul 2025 21:17:31 +0200
changeset 82929 77a3d8559288
parent 82928 90e4e9091531
child 82930 eea4394dca09
tuned signature; omit obsolete "force", following 2ca0c01164cd;
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 = {