tuned GUI: no scroll_bottom for completely different output;

--- 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) =