# HG changeset patch
# User wenzelm
# Date 1755979212 -7200
# Node ID 364feb78c4edda296d8a98467f2faae75d9aa782
# Parent  8c7599cd6a14e9d10d0c408223a99daf5455aa87
clarified AccessibleName, based on current buffer --- not the initial one;

diff -r 8c7599cd6a14 -r 364feb78c4ed src/Tools/jEdit/src/jedit_accessible.scala
--- a/src/Tools/jEdit/src/jedit_accessible.scala	Sat Aug 23 21:34:21 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_accessible.scala	Sat Aug 23 22:00:12 2025 +0200
@@ -12,8 +12,9 @@
 import isabelle._
 
 import org.gjt.sp.jedit
-import org.gjt.sp.jedit.{Buffer, ViewFactory}
+import org.gjt.sp.jedit.{jEdit, Buffer, ViewFactory}
 import org.gjt.sp.jedit.bufferset.BufferSet
+import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, JEditTextAreaFactory, TextArea => TextArea_JEdit,
   TextAreaPainter, TextAreaPainterFactory}
 
@@ -24,6 +25,20 @@
 
 
 object JEdit_Accessible {
+  def make_title(prefix: String, jbuffer: JEditBuffer): String = {
+    val suffix =
+      jbuffer match {
+        case buffer: Buffer =>
+          if (jEdit.getBooleanProperty("view.showFullPath") && !buffer.isNewFile) {
+            buffer.getPath(true)
+          }
+          else buffer.getName
+        case _ => ""
+      }
+    prefix + if_proper(prefix.nonEmpty && suffix.nonEmpty, " - ") + suffix
+  }
+
+
   /* view */
 
   class View_Factory extends ViewFactory {
@@ -31,13 +46,14 @@
       new View(buffer, config)
   }
 
-  class View(buffer: Buffer, config: jedit.View.ViewConfig) extends jedit.View(buffer, config) {
+  class View(buffer0: Buffer, config: jedit.View.ViewConfig) extends jedit.View(buffer0, config) {
     override def getAccessibleContext: AccessibleContext = {
       if (accessibleContext == null) { accessibleContext = new Accessible_Context }
       accessibleContext
     }
 
     class Accessible_Context extends AccessibleJFrame {
+      override def getAccessibleName: String = make_title(PIDE.title, getBuffer)
     }
   }
 
@@ -49,15 +65,15 @@
       new EditPane(view, bufferSetSource, buffer)
   }
 
-  class EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer: Buffer)
-      extends jedit.EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer: Buffer) {
+  class EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer0: Buffer)
+      extends jedit.EditPane(view: jedit.View, bufferSetSource: BufferSet, buffer0: Buffer) {
     override def getAccessibleContext: AccessibleContext = {
       if (accessibleContext == null) { accessibleContext = new Accessible_Context }
       accessibleContext
     }
 
     class Accessible_Context extends AccessibleJPanel {
-      override def getAccessibleName: String = "editor panel"
+      override def getAccessibleName: String = make_title("editor panel", getBuffer)
     }
   }
 
@@ -77,7 +93,7 @@
     }
 
     protected class Accessible_Context extends AccessibleJPanel {
-      override def getAccessibleName: String = "editor text"
+      override def getAccessibleName: String = make_title("editor text", buffer)
       override def getAccessibleRole: AccessibleRole = AccessibleRole.TEXT
       override def getAccessibleText: AccessibleText = accessible_text
       override def getAccessibleChildrenCount: Int = 0