# HG changeset patch
# User wenzelm
# Date 1739114186 -3600
# Node ID 74e14c621d44cc8753a8b3b5ba248d20f4a76e2b
# Parent  f6460ae54866405077fcd65e98e7db4da5adcf2a
tuned GUI: preserve horizontal scrollbar position;

diff -r f6460ae54866 -r 74e14c621d44 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Feb 09 14:54:35 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Feb 09 16:16:26 2025 +0100
@@ -199,6 +199,14 @@
             if (future_refresh.value.contains(current_refresh)) {
               current_rendering = rendering
 
+              val horizontal_offset = pretty_text_area.getHorizontalOffset
+
+              def scroll_to(offset: Int, x: Int = horizontal_offset): Unit = {
+                setCaretPosition(offset)
+                JEdit_Lib.scroll_to_caret(pretty_text_area)
+                pretty_text_area.setHorizontalOffset(x)
+              }
+
               val scroll_bottom = JEdit_Lib.scrollbar_bottom(pretty_text_area)
               val scroll_start = JEdit_Lib.scrollbar_start(pretty_text_area)
               val update_start =
@@ -208,11 +216,9 @@
                   JEdit_Lib.set_text(getBuffer, rich_texts.map(_.text))
                 }
 
-              setCaretPosition(
-                if (scroll_bottom) JEdit_Lib.bottom_line_offset(getBuffer)
-                else if (scroll_start < update_start) scroll_start
-                else 0)
-              JEdit_Lib.scroll_to_caret(pretty_text_area)
+              if (scroll_bottom) scroll_to(JEdit_Lib.bottom_line_offset(getBuffer))
+              else if (scroll_start < update_start) scroll_to(scroll_start)
+              else scroll_to(0, x = 0)
 
               val (search_update_start, search_results) =
                 current_search_results.update(update_start)