1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 20:16:12 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 21:32:45 2013 +0100
     1.3 @@ -10,7 +10,10 @@
     1.4  import isabelle._
     1.5  
     1.6  
     1.7 +import java.io.{File => JFile}
     1.8 +
     1.9  import org.gjt.sp.jedit.{jEdit, View}
    1.10 +import org.gjt.sp.jedit.browser.VFSBrowser
    1.11  
    1.12  
    1.13  class JEdit_Editor extends Editor[View]
    1.14 @@ -107,11 +110,11 @@
    1.15  
    1.16    /* hyperlinks */
    1.17  
    1.18 -  def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
    1.19 +  def goto(view: View, name: String, line: Int = 0, column: Int = 0)
    1.20    {
    1.21      Swing_Thread.require()
    1.22  
    1.23 -    JEdit_Lib.jedit_buffer(file_name) match {
    1.24 +    JEdit_Lib.jedit_buffer(name) match {
    1.25        case Some(buffer) =>
    1.26          view.goToBuffer(buffer)
    1.27          val text_area = view.getTextArea
    1.28 @@ -126,11 +129,14 @@
    1.29            case _: IllegalArgumentException =>
    1.30          }
    1.31  
    1.32 +      case None if (new JFile(name)).isDirectory =>
    1.33 +        VFSBrowser.browseDirectory(view, name)
    1.34 +
    1.35        case None =>
    1.36          val args =
    1.37 -          if (line <= 0) Array(file_name)
    1.38 -          else if (column <= 0) Array(file_name, "+line:" + line.toInt)
    1.39 -          else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
    1.40 +          if (line <= 0) Array(name)
    1.41 +          else if (column <= 0) Array(name, "+line:" + line.toInt)
    1.42 +          else Array(name, "+line:" + line.toInt + "," + column.toInt)
    1.43          jEdit.openFiles(view, null, args)
    1.44      }
    1.45    }
    1.46 @@ -146,8 +152,8 @@
    1.47            })
    1.48      }
    1.49  
    1.50 -  override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.51 -    new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
    1.52 +  override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.53 +    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
    1.54  
    1.55    override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
    1.56      : Option[Hyperlink] =