# HG changeset patch
# User wenzelm
# Date 1731495182 -3600
# Node ID 839c4b2b01fa83bbb34556771de018e527a7f0c9
# Parent  1935ed4fe9c2e15c442030c4b518b1dfce40f9a9
more ambitious scrolling: retain original scroll position if possible;

diff -r 1935ed4fe9c2 -r 839c4b2b01fa src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Nov 13 10:56:17 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Nov 13 11:53:02 2024 +0100
@@ -142,7 +142,7 @@
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
-  def set_text(buffer: JEditBuffer, text: List[String]): Unit = {
+  def set_text(buffer: JEditBuffer, text: List[String]): Int = {
     val old = buffer.isUndoInProgress
     def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
 
@@ -169,8 +169,10 @@
       set(true)
       buffer.beginCompoundEdit()
       val rest = drop_common_prefix(text)
+      val update_start = offset
       if (offset < length) buffer.remove(offset, length - offset)
       insert(rest)
+      update_start
     }
     finally {
       buffer.endCompoundEdit()
@@ -269,12 +271,15 @@
   def horizontal_scrollbar(text_area: TextArea): JScrollBar =
     Untyped.get[JScrollBar](text_area, "horizontal")
 
-  def scrollbar_at_bottom(text_area: TextArea): Boolean = {
-    val vertical = vertical_scrollbar(text_area)
-    vertical != null &&
-      vertical.getValue > 0 &&
-      vertical.getValue + vertical.getVisibleAmount == vertical.getMaximum
-  }
+  def scrollbar_at_end(scrollbar: JScrollBar): Boolean =
+    scrollbar.getValue > 0 &&
+      scrollbar.getValue + scrollbar.getVisibleAmount == scrollbar.getMaximum
+
+  def scrollbar_bottom(text_area: TextArea): Boolean =
+    scrollbar_at_end(vertical_scrollbar(text_area))
+
+  def scrollbar_start(text_area: TextArea): Int =
+    text_area.getBuffer.getLineStartOffset(vertical_scrollbar(text_area).getValue)
 
   def bottom_line_offset(buffer: JEditBuffer): Int =
     buffer.getLineStartOffset(buffer.getLineOfOffset(buffer.getLength))
diff -r 1935ed4fe9c2 -r 839c4b2b01fa src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 13 10:56:17 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 13 11:53:02 2024 +0100
@@ -118,13 +118,20 @@
                 results == current_base_results
             ) {
               current_rendering = rendering
-              val bottom = JEdit_Lib.scrollbar_at_bottom(pretty_text_area)
-              JEdit_Lib.buffer_edit(getBuffer) {
-                rich_text_area.active_reset()
-                getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
-                JEdit_Lib.set_text(getBuffer, rich_texts.map(_.text))
-              }
-              setCaretPosition(if (bottom) JEdit_Lib.bottom_line_offset(getBuffer) else 0)
+
+              val scroll_bottom = JEdit_Lib.scrollbar_bottom(pretty_text_area)
+              val scroll_start = JEdit_Lib.scrollbar_start(pretty_text_area)
+              val update_start =
+                JEdit_Lib.buffer_edit(getBuffer) {
+                  rich_text_area.active_reset()
+                  getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
+                  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)
             }
           }