observe buffer.isReadOnly;
authorwenzelm
Mon, 25 Aug 2025 20:43:02 +0200
changeset 83057 85251ccb7d2f
parent 83056 27290e754b1a
child 83058 77c3ecc6f562
observe buffer.isReadOnly;
src/Tools/jEdit/src/jedit_accessible.scala
--- a/src/Tools/jEdit/src/jedit_accessible.scala	Mon Aug 25 17:41:18 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_accessible.scala	Mon Aug 25 20:43:02 2025 +0200
@@ -202,7 +202,9 @@
         }
 
       override def getCharacterAttribute(i: Int): AttributeSet = SimpleAttributeSet.EMPTY
-      override def setAttributes(start: Int, stop: Int, att: AttributeSet): Unit = {}
+
+      override def setAttributes(start: Int, stop: Int, att: AttributeSet): Unit =
+        if (!buffer.isReadOnly) {}
 
       override def getSelectionStart: Int =
         if (text_area.getSelectionCount == 1) text_area.getSelection(0).getStart
@@ -220,49 +222,59 @@
         }
         else ""
 
-      override def selectText(start: Int, stop: Int): Unit = {
-        text_area.selectNone()
-        text_area.addToSelection(new Selection.Range(start min stop, start max stop))
-      }
+      override def selectText(start: Int, stop: Int): Unit =
+        if (!buffer.isReadOnly) {
+          text_area.selectNone()
+          text_area.addToSelection(new Selection.Range(start min stop, start max stop))
+        }
 
-      override def cut(start: Int, stop: Int): Unit = {
-        selectText(start, stop)
-        Registers.cut(text_area, '$')
-      }
+      override def cut(start: Int, stop: Int): Unit =
+        if (!buffer.isReadOnly) {
+          selectText(start, stop)
+          Registers.cut(text_area, '$')
+        }
 
-      override def paste(start: Int): Unit = {
-        selectText(start, start)
-        Registers.paste(text_area, '$')
-      }
+      override def paste(start: Int): Unit =
+        if (!buffer.isReadOnly) {
+          selectText(start, start)
+          Registers.paste(text_area, '$')
+        }
 
-      override def delete(start: Int, stop: Int): Unit = {
-        selectText(start, stop)
-        buffer.remove(start min stop, (stop - start).abs)
-      }
+      override def delete(start: Int, stop: Int): Unit =
+        if (!buffer.isReadOnly) {
+          selectText(start, stop)
+          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 =
-        JEdit_Lib.buffer_edit(buffer) {
-          text_area.selectNone()
-          buffer.remove(0, buffer.getLength)
-          buffer.insert(0, s)
+        if (!buffer.isReadOnly) {
+          JEdit_Lib.buffer_edit(buffer) {
+            text_area.selectNone()
+            buffer.remove(0, buffer.getLength)
+            buffer.insert(0, s)
+          }
         }
 
       override def insertTextAtIndex(start: Int, s: String): Unit =
-        JEdit_Lib.buffer_edit(buffer) {
-          selectText(start, start)
-          buffer.insert(start, s)
+        if (!buffer.isReadOnly) {
+          JEdit_Lib.buffer_edit(buffer) {
+            selectText(start, start)
+            buffer.insert(start, s)
+          }
         }
 
       override def replaceText(start: Int, stop: Int, s: String): Unit =
-        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)
+        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)
+          }
         }
     }
   }