8 package isabelle.jedit |
8 package isabelle.jedit |
9 |
9 |
10 |
10 |
11 import isabelle._ |
11 import isabelle._ |
12 |
12 |
13 import java.io.{File => JFile} |
|
14 |
|
15 import org.gjt.sp.jedit.{View, jEdit} |
13 import org.gjt.sp.jedit.{View, jEdit} |
16 import org.gjt.sp.jedit.textarea.JEditTextArea |
14 import org.gjt.sp.jedit.textarea.JEditTextArea |
17 |
15 |
18 |
16 |
19 object Hyperlink |
17 object Hyperlink |
20 { |
18 { |
21 def apply(file: JFile, line: Int, column: Int): Hyperlink = |
19 def apply(jedit_file: String, line: Int, column: Int): Hyperlink = |
22 File_Link(file, line, column) |
20 File_Link(jedit_file, line, column) |
23 } |
21 } |
24 |
22 |
25 abstract class Hyperlink |
23 abstract class Hyperlink |
26 { |
24 { |
27 def follow(view: View): Unit |
25 def follow(view: View): Unit |
28 } |
26 } |
29 |
27 |
30 private case class File_Link(file: JFile, line: Int, column: Int) extends Hyperlink |
28 private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink |
31 { |
29 { |
32 override def follow(view: View) |
30 override def follow(view: View) |
33 { |
31 { |
34 Swing_Thread.require() |
32 Swing_Thread.require() |
35 |
33 |
36 val full_name = file.getCanonicalPath |
34 Isabelle.jedit_buffer(jedit_file) match { |
37 val base_name = file.getName |
|
38 |
|
39 Isabelle.jedit_buffer(full_name) match { |
|
40 case Some(buffer) => |
35 case Some(buffer) => |
41 view.setBuffer(buffer) |
36 view.setBuffer(buffer) |
42 val text_area = view.getTextArea |
37 val text_area = view.getTextArea |
43 |
38 |
44 try { |
39 try { |
51 case _: IllegalArgumentException => |
46 case _: IllegalArgumentException => |
52 } |
47 } |
53 |
48 |
54 case None => |
49 case None => |
55 val args = |
50 val args = |
56 if (line <= 0) Array(base_name) |
51 if (line <= 0) Array(jedit_file) |
57 else if (column <= 0) Array(base_name, "+line:" + line.toInt) |
52 else if (column <= 0) Array(jedit_file, "+line:" + line.toInt) |
58 else Array(base_name, "+line:" + line.toInt + "," + column.toInt) |
53 else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt) |
59 jEdit.openFiles(view, file.getParent, args) |
54 jEdit.openFiles(view, null, args) |
60 } |
55 } |
61 } |
56 } |
62 } |
57 } |
63 |
58 |