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