--- a/src/Pure/GUI/tree_view.scala Thu Aug 21 20:09:16 2025 +0200
+++ b/src/Pure/GUI/tree_view.scala Thu Aug 21 20:53:05 2025 +0200
@@ -48,6 +48,7 @@
val root: Tree_View.Node = Tree_View.Node(),
single_selection_mode: Boolean = false
) extends JTree(root) {
+ getAccessibleContext.setAccessibleName(root.toString)
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 Thu Aug 21 20:09:16 2025 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 21 20:53:05 2025 +0200
@@ -20,6 +20,7 @@
private val doc_contents = Doc.contents(PIDE.ml_settings)
private val tree = new Tree_View(single_selection_mode = true)
+ tree.getAccessibleContext.setAccessibleName("Documentation")
for (section <- doc_contents.sections) {
tree.root.add(Tree_View.Node(section.title))