more standard treatment of AccessibleContext, following existing Swing components;
authorwenzelm
Fri, 22 Aug 2025 16:33:37 +0200
changeset 83032 a29b383ad733
parent 83031 ff3e034ff914
child 83033 1ac7cc481c4f
more standard treatment of AccessibleContext, following existing Swing components;
src/Pure/GUI/tree_view.scala
src/Tools/jEdit/src/documentation_dockable.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))
--- 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))