misc tuning;
authorwenzelm
Mon, 25 Aug 2025 20:46:06 +0200
changeset 83058 77c3ecc6f562
parent 83057 85251ccb7d2f
child 83059 10b1c49625f6
misc tuning;
src/Tools/jEdit/src/jedit_accessible.scala
--- a/src/Tools/jEdit/src/jedit_accessible.scala	Mon Aug 25 20:43:02 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_accessible.scala	Mon Aug 25 20:46:06 2025 +0200
@@ -201,10 +201,14 @@
           case _ => null
         }
 
-      override def getCharacterAttribute(i: Int): AttributeSet = SimpleAttributeSet.EMPTY
+      override def getTextRange(start: Int, stop: Int): String =
+        JEdit_Lib.get_text(buffer, Text.Range(start min stop, start max stop)).orNull
+
+      override def getCharacterAttribute(i: Int): AttributeSet =
+        SimpleAttributeSet.EMPTY  // FIXME
 
       override def setAttributes(start: Int, stop: Int, att: AttributeSet): Unit =
-        if (!buffer.isReadOnly) {}
+        if (!buffer.isReadOnly) {}  // FIXME
 
       override def getSelectionStart: Int =
         if (text_area.getSelectionCount == 1) text_area.getSelection(0).getStart
@@ -246,9 +250,6 @@
           buffer.remove(start min stop, (stop - start).abs)
         }
 
-      override def getTextRange(start: Int, stop: Int): String =
-        JEdit_Lib.get_text(buffer, Text.Range(start min stop, start max stop)).orNull
-
       override def setTextContents(s: String): Unit =
         if (!buffer.isReadOnly) {
           JEdit_Lib.buffer_edit(buffer) {
@@ -270,10 +271,8 @@
         if (!buffer.isReadOnly) {
           JEdit_Lib.buffer_edit(buffer) {
             selectText(start, stop)
-            val a = start min stop
-            val b = start max stop
-            buffer.remove(a, b - a)
-            buffer.insert(a, s)
+            buffer.remove(start min stop, (start - stop).abs)
+            buffer.insert(start min stop, s)
           }
         }
     }