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 def subdirs(file: File): List[File] = { |
34 override def click(view: View) = { |
35 val subs = file.listFiles.filter(_.isDirectory).toList |
35 Isabelle.system.source_file(ref_file) match { |
36 subs ::: subs.flatMap(subdirs) |
36 case None => System.err.println("Could not find source file " + ref_file) |
37 } |
37 case Some(file) => |
38 |
|
39 val srcs = List(new File(Isabelle.system.getenv("ML_SOURCES"))) |
|
40 val rec_srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src")) |
|
41 |
|
42 override def click(view: View) = |
|
43 (srcs ::: rec_srcs.flatMap(subdirs)).find(new File(_, ref_file).exists) match { |
|
44 case None => System.err.println("Could not find file " + ref_file) |
|
45 case Some(dir) => |
|
46 val file = new File(dir, ref_file) |
|
47 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
38 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
48 } |
39 } |
|
40 } |
49 } |
41 } |
50 |
42 |
51 class IsabelleHyperlinkSource extends HyperlinkSource |
43 class IsabelleHyperlinkSource extends HyperlinkSource |
52 { |
44 { |
53 def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { |
45 def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { |