more standard treatment of AccessibleContext, following existing Swing components;
--- 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))