# HG changeset patch
# User immler@in.tum.de
# Date 1243255000 -7200
# Node ID daa397b6401ce9e4659ced8f0904312315f41055
# Parent  c3bdaea2dd6ae793b8bbc74443f92d6e5430a853
changed handling of subdirectories

diff -r c3bdaea2dd6a -r daa397b6401c src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 17:36:45 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Mon May 25 14:36:40 2009 +0200
@@ -31,28 +31,21 @@
 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
+  def subdirs(file: File): List[File] = {
+    val subs = file.listFiles.filter(_.isDirectory).toList
+    subs ::: subs.flatMap(subdirs)
   }
 
-  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 _ =>
-      }
-  }
+  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)
+        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+    }
 }
 
 class IsabelleHyperlinkSource extends HyperlinkSource