equal
deleted
inserted
replaced
26 |
26 |
27 class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int) |
27 class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int) |
28 extends AbstractHyperlink(start, end, line, "") |
28 extends AbstractHyperlink(start, end, line, "") |
29 { |
29 { |
30 override def click(view: View) = { |
30 override def click(view: View) = { |
31 Isabelle.system.source_file(Path.explode(def_file)) match { |
31 Isabelle_System.source_file(Path.explode(def_file)) match { |
32 case None => |
32 case None => |
33 Library.error_dialog(view, "File not found", "Could not find source file " + def_file) |
33 Library.error_dialog(view, "File not found", "Could not find source file " + def_file) |
34 case Some(file) => |
34 case Some(file) => |
35 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line)) |
35 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line)) |
36 } |
36 } |