# HG changeset patch
# User wenzelm
# Date 1244146082 -7200
# Node ID 782b1948aca99b672b2564a0008b7718c372a4b5
# Parent  f37cd618f58217ba2f03950861daf53661c2e8c4
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b

diff -r f37cd618f582 -r 782b1948aca9 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Thu Jun 04 22:06:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Thu Jun 04 22:08:02 2009 +0200
@@ -31,21 +31,13 @@
 class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
-  def subdirs(file: File): List[File] = {
-    val subs = file.listFiles.filter(_.isDirectory).toList
-    subs ::: subs.flatMap(subdirs)
-  }
-
-  val srcs = List(new File(Isabelle.system.getenv("ML_SOURCES")))
-  val rec_srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"))
-
-  override def click(view: View) =
-    (srcs ::: rec_srcs.flatMap(subdirs)).find(new File(_, ref_file).exists) match {
-      case None => System.err.println("Could not find file " + ref_file)
-      case Some(dir) =>
-        val file = new File(dir, ref_file)
+  override def click(view: View) = {
+    Isabelle.system.source_file(ref_file) match {
+      case None => System.err.println("Could not find source file " + ref_file)
+      case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
     }
+  }
 }
 
 class IsabelleHyperlinkSource extends HyperlinkSource