# HG changeset patch
# User wenzelm
# Date 1407871790 -7200
# Node ID c1953856cfcaf2ea0c4f255714ce8b91aba127f6
# Parent  a2a7c1de4752775fd5b6fa62b47d8281973bdd11
clarified focus and key handling -- more like SideKick;
avoid resetting input map with its potentially confusion propagation of key events to unrelated components, e.g. main text area or tree scrollbar;

diff -r a2a7c1de4752 -r c1953856cfca src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 20:42:39 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 21:29:50 2014 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Dimension, GridLayout}
-import java.awt.event.{MouseEvent, MouseAdapter}
+import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.{JTree, JScrollPane, JComponent}
 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
@@ -47,38 +47,57 @@
 
   private val tree = new JTree(root)
 
-  for (cond <-
-    List(JComponent.WHEN_FOCUSED,
-      JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
-      JComponent.WHEN_IN_FOCUSED_WINDOW)) tree.setInputMap(cond, null)
+  override def focusOnDefaultComponent { tree.requestFocusInWindow }
 
   if (!OperatingSystem.isMacOSLF)
     tree.putClientProperty("JTree.lineStyle", "Angled")
   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+
+  private def action(node: DefaultMutableTreeNode)
+  {
+    node.getUserObject match {
+      case Text_File(_, path) =>
+        PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
+      case Documentation(_, _, path) =>
+        if (path.is_file)
+          PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
+        else {
+          Future.fork {
+            try { Doc.view(path) }
+            catch {
+              case exn: Throwable =>
+                GUI.error_dialog(view,
+                  "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+            }
+          }
+        }
+      case _ =>
+    }
+  }
+
+  tree.addKeyListener(new KeyAdapter {
+    override def keyPressed(e: KeyEvent)
+    {
+      if (e.getKeyCode == KeyEvent.VK_ENTER) {
+        e.consume
+        val path = tree.getSelectionPath
+        if (path != null) {
+          path.getLastPathComponent match {
+            case node: DefaultMutableTreeNode => action(node)
+            case _ =>
+          }
+        }
+      }
+    }
+  })
   tree.addMouseListener(new MouseAdapter {
-    override def mouseClicked(e: MouseEvent) {
+    override def mouseClicked(e: MouseEvent)
+    {
       val click = tree.getPathForLocation(e.getX, e.getY)
       if (click != null && e.getClickCount == 1) {
         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
-            node.getUserObject match {
-              case Text_File(_, path) =>
-                PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
-              case Documentation(_, _, path) =>
-                if (path.is_file)
-                  PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
-                else {
-                  Future.fork {
-                    try { Doc.view(path) }
-                    catch {
-                      case exn: Throwable =>
-                        GUI.error_dialog(view,
-                          "Documentation error", GUI.scrollable_text(Exn.message(exn)))
-                    }
-                  }
-                }
-              case _ =>
-            }
+            action(node)
           case _ =>
         }
       }