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