# HG changeset patch
# User wenzelm
# Date 1753714992 -7200
# Node ID b07201796c1e04484bfeff6a871ac6bfc5d96302
# Parent  cfc15a2c1f1e31712c8b5fe614ddb1965a8c71e5
more tuning and simplification (see 6dabae94cf57);

diff -r cfc15a2c1f1e -r b07201796c1e src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 16:33:55 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 28 17:03:12 2025 +0200
@@ -35,15 +35,12 @@
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
 
-  private def handle_update(
-    follow: Boolean = true,
-    restriction: Option[Set[Command]] = None
-  ): Unit = {
+  private def handle_update(restriction: Option[Set[Command]] = None): Unit = {
     GUI_Thread.require {}
 
     for {
       snapshot <- PIDE.editor.current_node_snapshot(view)
-      if follow && !snapshot.is_outdated
+      if !snapshot.is_outdated
       command <- PIDE.editor.current_command(view, snapshot)
       if restriction.isEmpty || restriction.get.contains(command)
     } {
@@ -70,7 +67,7 @@
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       do_update = state
-      handle_update(follow = do_update)
+      if (do_update) handle_update()
     }
   }
 
@@ -96,15 +93,15 @@
           output.handle_resize()
           output_state_button.load()
           auto_hovering_button.load()
-          handle_update(do_update)
+          if (do_update) handle_update()
         }
 
       case changed: Session.Commands_Changed =>
         val restriction = if (changed.assignment) None else Some(changed.commands)
-        GUI_Thread.later { handle_update(follow = do_update, restriction = restriction) }
+        GUI_Thread.later { if (do_update) handle_update(restriction = restriction) }
 
       case Session.Caret_Focus =>
-        GUI_Thread.later { handle_update(follow = do_update) }
+        GUI_Thread.later { if (do_update) handle_update() }
     }
 
   override def init(): Unit = {