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