# HG changeset patch
# User wenzelm
# Date 1730887518 -3600
# Node ID 9863ddead037b104ed20669b720a25f058075227
# Parent  a1567e05f7fda969895c7069af4c5b804369b4fb
misc tuning;

diff -r a1567e05f7fd -r 9863ddead037 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 05 23:51:44 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Wed Nov 06 11:05:18 2024 +0100
@@ -23,15 +23,14 @@
 
   for (section <- doc_contents.sections) {
     tree.root.add(Tree_View.Node(section.title))
-    for (entry <- section.entries) {
-      tree.root.getLastChild.asInstanceOf[Tree_View.Node].add(Tree_View.Node(entry))
-    }
+    val last_node = tree.root.getLastChild.asInstanceOf[Tree_View.Node]
+    for (entry <- section.entries) last_node.add(Tree_View.Node(entry))
   }
 
   override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
 
-  private def action(node: Tree_View.Node): Unit = {
-    node match {
+  private def action(obj: AnyRef): Unit = {
+    obj match {
       case Tree_View.Node(entry: Doc.Entry) =>
         if (entry.path.is_pdf) PIDE.editor.goto_doc(view, entry.path)
         else PIDE.editor.goto_file(true, view, File.platform_path(entry.path))
@@ -44,12 +43,7 @@
       if (e.getKeyCode == KeyEvent.VK_ENTER) {
         e.consume()
         val path = tree.getSelectionPath
-        if (path != null) {
-          path.getLastPathComponent match {
-            case node: Tree_View.Node => action(node)
-            case _ =>
-          }
-        }
+        if (path != null) action(path.getLastPathComponent)
       }
     }
   })
@@ -57,10 +51,9 @@
     override def mouseClicked(e: MouseEvent): Unit = {
       val click = tree.getPathForLocation(e.getX, e.getY)
       if (click != null && e.getClickCount == 1) {
-        (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
-          case (node: Tree_View.Node, node1: Tree_View.Node) if node == node1 => action(node)
-          case _ =>
-        }
+        val click_node = click.getLastPathComponent
+        val path_node = tree.getLastSelectedPathComponent
+        if (click_node == path_node) action(click_node)
       }
     }
   })