# HG changeset patch
# User wenzelm
# Date 1316463231 -7200
# Node ID d88f7fc62a405bcdb106f6b60c7fceaeec75678e
# Parent  3aa261a3c7d6ff059ac2298a365a580b2ac8bd13
double clicks switch to document node buffer;

diff -r 3aa261a3c7d6 -r d88f7fc62a40 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:53:07 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 22:13:51 2011 +0200
@@ -12,7 +12,7 @@
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
   ScrollPane, TabbedPane, Component, Swing}
-import scala.swing.event.{ButtonClicked, SelectionChanged}
+import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Insets}
@@ -29,7 +29,14 @@
   private val readme = new HTML_Panel("SansSerif", 14)
   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
-  val status = new ListView(Nil: List[Document.Node.Name])
+  val status = new ListView(Nil: List[Document.Node.Name]) {
+    listenTo(mouse.clicks)
+    reactions += {
+      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
+        val index = peer.locationToIndex(point)
+        if (index >= 0) jEdit.openFile(view, listData(index).node)
+    }
+  }
   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   status.selection.intervalMode = ListView.IntervalMode.Single