29 } |
29 } |
30 |
30 |
31 class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int) |
31 class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int) |
32 extends AbstractHyperlink(start, end, line, "") |
32 extends AbstractHyperlink(start, end, line, "") |
33 { |
33 { |
34 val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"), |
34 def subdirs(file: File): List[File] = { |
35 new File(Isabelle.system.getenv("ML_SOURCES"))) |
35 val subs = file.listFiles.filter(_.isDirectory).toList |
36 |
36 subs ::: subs.flatMap(subdirs) |
37 def find_file(file: File, filename: String): Option[File] = |
|
38 { |
|
39 if (file.getName == new File(filename).getName) Some(file) |
|
40 else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None) |
|
41 else None |
|
42 } |
37 } |
43 |
38 |
44 override def click(view: View) = { |
39 val srcs = List(new File(Isabelle.system.getenv("ML_SOURCES"))) |
45 srcs.find(src => |
40 val rec_srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src")) |
46 find_file(src, ref_file) match { |
41 |
47 case None => false |
42 override def click(view: View) = |
48 case Some(file) => |
43 (srcs ::: rec_srcs.flatMap(subdirs)).find(new File(_, ref_file).exists) match { |
49 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
44 case None => System.err.println("Could not find file " + ref_file) |
50 true}) |
45 case Some(dir) => |
51 match { |
46 val file = new File(dir, ref_file) |
52 case None => System.err.println("Could not find file " + ref_file) |
47 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
53 case _ => |
48 } |
54 } |
|
55 } |
|
56 } |
49 } |
57 |
50 |
58 class IsabelleHyperlinkSource extends HyperlinkSource |
51 class IsabelleHyperlinkSource extends HyperlinkSource |
59 { |
52 { |
60 def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { |
53 def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { |