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