equal
deleted
inserted
replaced
21 import isabelle.prover.RefInfo |
21 import isabelle.prover.RefInfo |
22 |
22 |
23 class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int) |
23 class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int) |
24 extends AbstractHyperlink(start, end, line, "") |
24 extends AbstractHyperlink(start, end, line, "") |
25 { |
25 { |
26 override def click(view: View) = { |
26 override def click(view: View) { |
27 view.getTextArea.moveCaretPosition(ref_offset) |
27 view.getTextArea.moveCaretPosition(ref_offset) |
28 } |
28 } |
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) |