# HG changeset patch
# User wenzelm
# Date 1753715126 -7200
# Node ID a9ba368906221979e5d718dc41a748924156f5b0
# Parent  b07201796c1e04484bfeff6a871ac6bfc5d96302
tuned;

diff -r b07201796c1e -r a9ba36890622 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 17:03:12 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 17:05:26 2025 +0200
@@ -35,23 +35,22 @@
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
 
-  private def handle_update(restriction: Option[Set[Command]] = None): Unit = {
-    GUI_Thread.require {}
-
-    for {
-      snapshot <- PIDE.editor.current_node_snapshot(view)
-      if !snapshot.is_outdated
-      command <- PIDE.editor.current_command(view, snapshot)
-      if restriction.isEmpty || restriction.get.contains(command)
-    } {
-      val results = snapshot.command_results(command)
-      val new_output = Rendering.output_messages(results, JEdit_Options.output_state())
-      if (current_output != new_output) {
-        output.pretty_text_area.update(snapshot, results, new_output)
-        current_output = new_output
+  private def handle_update(restriction: Option[Set[Command]] = None): Unit =
+    GUI_Thread.require {
+      for {
+        snapshot <- PIDE.editor.current_node_snapshot(view)
+        if !snapshot.is_outdated
+        command <- PIDE.editor.current_command(view, snapshot)
+        if restriction.isEmpty || restriction.get.contains(command)
+      } {
+        val results = snapshot.command_results(command)
+        val new_output = Rendering.output_messages(results, JEdit_Options.output_state())
+        if (current_output != new_output) {
+          output.pretty_text_area.update(snapshot, results, new_output)
+          current_output = new_output
+        }
       }
     }
-  }
 
   output.setup(dockable)
   dockable.set_content(output.split_pane)