1.1 --- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 14:47:57 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 16:47:11 2009 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4   */
     1.5  
     1.6  package isabelle.jedit
     1.7 +
     1.8 +import java.io.File
     1.9 +
    1.10  import gatchan.jedit.hyperlinks.Hyperlink
    1.11  import gatchan.jedit.hyperlinks.HyperlinkSource
    1.12  import gatchan.jedit.hyperlinks.AbstractHyperlink
    1.13 @@ -18,13 +21,40 @@
    1.14  import isabelle.prover.RefInfo
    1.15  
    1.16  class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    1.17 -  extends AbstractHyperlink(start, end, line, "tooltip")
    1.18 +  extends AbstractHyperlink(start, end, line, "")
    1.19  {
    1.20    override def click(view: View) = {
    1.21      view.getTextArea.moveCaretPosition(ref_offset)
    1.22    }
    1.23  }
    1.24  
    1.25 +class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    1.26 +  extends AbstractHyperlink(start, end, line, "")
    1.27 +{
    1.28 +  val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"),
    1.29 +                  new File(Isabelle.system.getenv("ML_SOURCES")))
    1.30 +
    1.31 +  def find_file(file: File, filename: String): Option[File] =
    1.32 +  {
    1.33 +    if (file.getName == new File(filename).getName) Some(file)
    1.34 +    else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None)
    1.35 +    else None
    1.36 +  }
    1.37 +
    1.38 +  override def click(view: View) = {
    1.39 +    srcs.find(src =>
    1.40 +      find_file(src, ref_file) match {
    1.41 +        case None => false
    1.42 +        case Some(file) =>
    1.43 +          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    1.44 +          true})
    1.45 +      match {
    1.46 +        case None => System.err.println("Could not find file " + ref_file)
    1.47 +        case _ =>
    1.48 +      }
    1.49 +  }
    1.50 +}
    1.51 +
    1.52  class IsabelleHyperlinkSource extends HyperlinkSource
    1.53  {
    1.54  	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
    1.55 @@ -46,8 +76,8 @@
    1.56            val line = buffer.getLineOfOffset(start)
    1.57            val end = theory_view.to_current(document, ref.abs_stop(document))
    1.58            ref.info match {
    1.59 -            case RefInfo(Some(file), Some(ref_line), _, _) =>
    1.60 -              null
    1.61 +            case RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    1.62 +              new ExternalHyperlink(start, end, line, ref_file, ref_line)
    1.63              case RefInfo(_, _, Some(id), Some(offset)) =>
    1.64                prover.get.command(id) match {
    1.65                  case Some(ref_cmd) =>