# HG changeset patch
# User wenzelm
# Date 1755873217 -7200
# Node ID a29b383ad7333c74dbc577eb77df0f7050c80187
# Parent  ff3e034ff914fb899fa53c4d58de83fba0646d9c
more standard treatment of AccessibleContext, following existing Swing components;

diff -r ff3e034ff914 -r a29b383ad733 src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Fri Aug 22 16:01:09 2025 +0200
+++ b/src/Pure/GUI/tree_view.scala	Fri Aug 22 16:33:37 2025 +0200
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import javax.accessibility.AccessibleContext
+
 import javax.swing.JTree
 import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel,
   TreeSelectionModel, DefaultTreeCellRenderer}
@@ -46,9 +48,19 @@
 
 class Tree_View(
   val root: Tree_View.Node = Tree_View.Node(),
-  single_selection_mode: Boolean = false
+  single_selection_mode: Boolean = false,
+  accessible_name: String = ""
 ) extends JTree(root) {
-  getAccessibleContext.setAccessibleName(root.toString)
+
+  override def getAccessibleContext: AccessibleContext = {
+    if (accessibleContext == null) { accessibleContext = new Accessible_Context }
+    accessibleContext
+  }
+  class Accessible_Context extends AccessibleJTree {
+    override def getAccessibleName: String =
+      proper_string(accessible_name).getOrElse(proper_string(root.toString).orNull)
+  }
+
   def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
     getLastSelectedPathComponent match {
       case Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj))
diff -r ff3e034ff914 -r a29b383ad733 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Aug 22 16:01:09 2025 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Aug 22 16:33:37 2025 +0200
@@ -19,8 +19,7 @@
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
   private val doc_contents = Doc.contents(PIDE.ml_settings)
 
-  private val tree = new Tree_View(single_selection_mode = true)
-  tree.getAccessibleContext.setAccessibleName("Documentation")
+  private val tree = new Tree_View(single_selection_mode = true, accessible_name = "Documentation")
 
   for (section <- doc_contents.sections) {
     tree.root.add(Tree_View.Node(section.title))