# HG changeset patch
# User wenzelm
# Date 1739114660 -3600
# Node ID a6a3ba4f715732a3163c2b8130c163c159bf6246
# Parent  74e14c621d44cc8753a8b3b5ba248d20f4a76e2b
tuned GUI: no scroll_bottom for completely different output;

diff -r 74e14c621d44 -r a6a3ba4f7157 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Feb 09 16:16:26 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Feb 09 16:24:20 2025 +0100
@@ -216,8 +216,10 @@
                   JEdit_Lib.set_text(getBuffer, rich_texts.map(_.text))
                 }
 
-              if (scroll_bottom) scroll_to(JEdit_Lib.bottom_line_offset(getBuffer))
-              else if (scroll_start < update_start) scroll_to(scroll_start)
+              if (update_start > 0 && scroll_bottom) {
+                scroll_to(JEdit_Lib.bottom_line_offset(getBuffer))
+              }
+              else if (update_start > scroll_start) scroll_to(scroll_start)
               else scroll_to(0, x = 0)
 
               val (search_update_start, search_results) =