# HG changeset patch
# User wenzelm
# Date 1743789172 -7200
# Node ID af78b84151ed3b1d23f0d5a8c3035d8b1eec4d89
# Parent  21f7f29ef9cbc3d953ac8dd4c010b237f381dad6
more uniform treatment of open buffer vs. loaded file (NB: setCaretPosition includes selectionNone);

diff -r 21f7f29ef9cb -r af78b84151ed src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 17:31:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 19:52:52 2025 +0200
@@ -129,7 +129,7 @@
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
         if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
-        view.getTextArea.moveCaretPosition(buffer_offset(buffer))
+        view.getTextArea.setCaretPosition(buffer_offset(buffer))
 
       case None =>
         val is_dir =