# HG changeset patch
# User wenzelm
# Date 1753726513 -7200
# Node ID 31478aedef9086ffaa0726861f4ac287eb67b914
# Parent  f4bc5313c8216d2d3f37982686d0b04e946fd77b
tuned;

diff -r f4bc5313c821 -r 31478aedef90 src/Tools/VSCode/src/dynamic_output.scala
--- 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)
   }