1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:53:07 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 22:13:51 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  import scala.actors.Actor._
     1.5  import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     1.6    ScrollPane, TabbedPane, Component, Swing}
     1.7 -import scala.swing.event.{ButtonClicked, SelectionChanged}
     1.8 +import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
     1.9  
    1.10  import java.lang.System
    1.11  import java.awt.{BorderLayout, Graphics2D, Insets}
    1.12 @@ -29,7 +29,14 @@
    1.13    private val readme = new HTML_Panel("SansSerif", 14)
    1.14    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    1.15  
    1.16 -  val status = new ListView(Nil: List[Document.Node.Name])
    1.17 +  val status = new ListView(Nil: List[Document.Node.Name]) {
    1.18 +    listenTo(mouse.clicks)
    1.19 +    reactions += {
    1.20 +      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    1.21 +        val index = peer.locationToIndex(point)
    1.22 +        if (index >= 0) jEdit.openFile(view, listData(index).node)
    1.23 +    }
    1.24 +  }
    1.25    status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    1.26    status.selection.intervalMode = ListView.IntervalMode.Single
    1.27