# HG changeset patch
# User wenzelm
# Date 1731491777 -3600
# Node ID 1935ed4fe9c2e15c442030c4b518b1dfce40f9a9
# Parent  c3793899b8805f98274d426f794645c1f74fe1df
more ambitious scrolling: retain bottom position after output;

diff -r c3793899b880 -r 1935ed4fe9c2 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Nov 12 22:30:45 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Nov 13 10:56:17 2024 +0100
@@ -12,7 +12,7 @@
 import java.io.{File => JFile}
 import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
-import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
+import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow, SwingUtilities}
 
 import scala.util.parsing.input.CharSequenceReader
 import scala.jdk.CollectionConverters._
@@ -261,6 +261,34 @@
   }
 
 
+  /* scrolling */
+
+  def vertical_scrollbar(text_area: TextArea): JScrollBar =
+    Untyped.get[JScrollBar](text_area, "vertical")
+
+  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 bottom_line_offset(buffer: JEditBuffer): Int =
+    buffer.getLineStartOffset(buffer.getLineOfOffset(buffer.getLength))
+
+  def scroll_to_caret(text_area: TextArea): Unit = {
+    val caret_line = text_area.getCaretLine()
+    val display_manager = text_area.getDisplayManager
+    if (!display_manager.isLineVisible(caret_line)) {
+      display_manager.expandFold(caret_line, true)
+    }
+    text_area.scrollToCaret(true)
+  }
+
+
   /* graphics range */
 
   def font_metric(painter: TextAreaPainter): Font_Metric =
diff -r c3793899b880 -r 1935ed4fe9c2 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 12 22:30:45 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 13 10:56:17 2024 +0100
@@ -118,12 +118,14 @@
                 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(0)
               }
+              setCaretPosition(if (bottom) JEdit_Lib.bottom_line_offset(getBuffer) else 0)
+              JEdit_Lib.scroll_to_caret(pretty_text_area)
             }
           }
         })