# HG changeset patch
# User immler@in.tum.de
# Date 1243003631 -7200
# Node ID 15abc5f5f40a8b1d46f1be85f9c778017321f07f
# Parent  b517d06072977b7820625243f395d13ef1e9e50e
implemented links to other files

diff -r b517d0607297 -r 15abc5f5f40a src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 14:47:57 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 16:47:11 2009 +0200
@@ -6,6 +6,9 @@
  */
 
 package isabelle.jedit
+
+import java.io.File
+
 import gatchan.jedit.hyperlinks.Hyperlink
 import gatchan.jedit.hyperlinks.HyperlinkSource
 import gatchan.jedit.hyperlinks.AbstractHyperlink
@@ -18,13 +21,40 @@
 import isabelle.prover.RefInfo
 
 class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
-  extends AbstractHyperlink(start, end, line, "tooltip")
+  extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) = {
     view.getTextArea.moveCaretPosition(ref_offset)
   }
 }
 
+class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
+  extends AbstractHyperlink(start, end, line, "")
+{
+  val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"),
+                  new File(Isabelle.system.getenv("ML_SOURCES")))
+
+  def find_file(file: File, filename: String): Option[File] =
+  {
+    if (file.getName == new File(filename).getName) Some(file)
+    else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None)
+    else None
+  }
+
+  override def click(view: View) = {
+    srcs.find(src =>
+      find_file(src, ref_file) match {
+        case None => false
+        case Some(file) =>
+          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+          true})
+      match {
+        case None => System.err.println("Could not find file " + ref_file)
+        case _ =>
+      }
+  }
+}
+
 class IsabelleHyperlinkSource extends HyperlinkSource
 {
 	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
@@ -46,8 +76,8 @@
           val line = buffer.getLineOfOffset(start)
           val end = theory_view.to_current(document, ref.abs_stop(document))
           ref.info match {
-            case RefInfo(Some(file), Some(ref_line), _, _) =>
-              null
+            case RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+              new ExternalHyperlink(start, end, line, ref_file, ref_line)
             case RefInfo(_, _, Some(id), Some(offset)) =>
               prover.get.command(id) match {
                 case Some(ref_cmd) =>