tuned;

--- a/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:13:46 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Mon Jul 28 20:15:13 2025 +0200
@@ -20,7 +20,7 @@
     pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
 
   private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
-    val output =
+    val maybe_output =
       server.resources.get_caret() match {
         case None => Some(Nil)
         case Some(caret) =>
@@ -35,10 +35,7 @@
           }
       }
       
-    output match {
-      case None =>
-      case Some(output) => pretty_panel.refresh(output)
-    }
+    maybe_output.foreach(pretty_panel.refresh)
   }