# HG changeset patch
# User wenzelm
# Date 1386368738 -3600
# Node ID 070d5e8567983af1a75c2d7a0c97f5105b6f43a7
# Parent  a9c9792e87a59e34060d2db06e6ef72bf9f4f38c
directly react on click, assuming that document view operation is mostly idempotent;

diff -r a9c9792e87a5 -r 070d5e856798 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Dec 06 22:50:47 2013 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Dec 06 23:25:38 2013 +0100
@@ -10,6 +10,7 @@
 import isabelle._
 
 import java.awt.{Dimension, GridLayout}
+import java.awt.event.{MouseEvent, MouseAdapter}
 import javax.swing.{JTree, JScrollPane}
 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
@@ -48,12 +49,12 @@
   if (!OperatingSystem.isMacOSLF)
     tree.putClientProperty("JTree.lineStyle", "Angled")
   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
-  tree.addTreeSelectionListener(
-    new TreeSelectionListener {
-      override def valueChanged(e: TreeSelectionEvent)
-      {
-        tree.getLastSelectedPathComponent match {
-          case node: DefaultMutableTreeNode =>
+  tree.addMouseListener(new MouseAdapter {
+    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 Documentation(name, _) =>
                 default_thread_pool.submit(() =>
@@ -70,7 +71,8 @@
           case _ =>
         }
       }
-    })
+    }
+  })
   tree.setRootVisible(false)
   tree.setVisibleRowCount(docs.length)
   (0 until docs.length).foreach(tree.expandRow)