clarified focus and key handling -- more like SideKick;
authorwenzelm
Tue Aug 12 21:29:50 2014 +0200 (2014-08-12)
changeset 57920c1953856cfca
parent 57919 a2a7c1de4752
child 57921 9225b2761126
child 57923 cdae2467311d
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;
src/Tools/jEdit/src/documentation_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 20:42:39 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 21:29:50 2014 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Dimension, GridLayout}
     1.7 -import java.awt.event.{MouseEvent, MouseAdapter}
     1.8 +import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
     1.9  import javax.swing.{JTree, JScrollPane, JComponent}
    1.10  import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
    1.11  import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
    1.12 @@ -47,38 +47,57 @@
    1.13  
    1.14    private val tree = new JTree(root)
    1.15  
    1.16 -  for (cond <-
    1.17 -    List(JComponent.WHEN_FOCUSED,
    1.18 -      JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
    1.19 -      JComponent.WHEN_IN_FOCUSED_WINDOW)) tree.setInputMap(cond, null)
    1.20 +  override def focusOnDefaultComponent { tree.requestFocusInWindow }
    1.21  
    1.22    if (!OperatingSystem.isMacOSLF)
    1.23      tree.putClientProperty("JTree.lineStyle", "Angled")
    1.24    tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
    1.25 +
    1.26 +  private def action(node: DefaultMutableTreeNode)
    1.27 +  {
    1.28 +    node.getUserObject match {
    1.29 +      case Text_File(_, path) =>
    1.30 +        PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    1.31 +      case Documentation(_, _, path) =>
    1.32 +        if (path.is_file)
    1.33 +          PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    1.34 +        else {
    1.35 +          Future.fork {
    1.36 +            try { Doc.view(path) }
    1.37 +            catch {
    1.38 +              case exn: Throwable =>
    1.39 +                GUI.error_dialog(view,
    1.40 +                  "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    1.41 +            }
    1.42 +          }
    1.43 +        }
    1.44 +      case _ =>
    1.45 +    }
    1.46 +  }
    1.47 +
    1.48 +  tree.addKeyListener(new KeyAdapter {
    1.49 +    override def keyPressed(e: KeyEvent)
    1.50 +    {
    1.51 +      if (e.getKeyCode == KeyEvent.VK_ENTER) {
    1.52 +        e.consume
    1.53 +        val path = tree.getSelectionPath
    1.54 +        if (path != null) {
    1.55 +          path.getLastPathComponent match {
    1.56 +            case node: DefaultMutableTreeNode => action(node)
    1.57 +            case _ =>
    1.58 +          }
    1.59 +        }
    1.60 +      }
    1.61 +    }
    1.62 +  })
    1.63    tree.addMouseListener(new MouseAdapter {
    1.64 -    override def mouseClicked(e: MouseEvent) {
    1.65 +    override def mouseClicked(e: MouseEvent)
    1.66 +    {
    1.67        val click = tree.getPathForLocation(e.getX, e.getY)
    1.68        if (click != null && e.getClickCount == 1) {
    1.69          (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
    1.70            case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
    1.71 -            node.getUserObject match {
    1.72 -              case Text_File(_, path) =>
    1.73 -                PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    1.74 -              case Documentation(_, _, path) =>
    1.75 -                if (path.is_file)
    1.76 -                  PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    1.77 -                else {
    1.78 -                  Future.fork {
    1.79 -                    try { Doc.view(path) }
    1.80 -                    catch {
    1.81 -                      case exn: Throwable =>
    1.82 -                        GUI.error_dialog(view,
    1.83 -                          "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    1.84 -                    }
    1.85 -                  }
    1.86 -                }
    1.87 -              case _ =>
    1.88 -            }
    1.89 +            action(node)
    1.90            case _ =>
    1.91          }
    1.92        }