1 /* Title: Tools/jEdit/src/jedit/isabelle_hyperlinks.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 |
|
4 Hyperlink setup for Isabelle proof documents. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.io.File |
|
13 |
|
14 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink} |
|
15 |
|
16 import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities} |
|
17 |
|
18 |
|
19 private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int) |
|
20 extends AbstractHyperlink(start, end, line, "") |
|
21 { |
|
22 override def click(view: View) { |
|
23 view.getTextArea.moveCaretPosition(def_offset) |
|
24 } |
|
25 } |
|
26 |
|
27 class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int) |
|
28 extends AbstractHyperlink(start, end, line, "") |
|
29 { |
|
30 override def click(view: View) = { |
|
31 Isabelle.system.source_file(def_file) match { |
|
32 case None => |
|
33 Library.error_dialog(view, "File not found", "Could not find source file " + def_file) |
|
34 case Some(file) => |
|
35 jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line)) |
|
36 } |
|
37 } |
|
38 } |
|
39 |
|
40 class Isabelle_Hyperlinks extends HyperlinkSource |
|
41 { |
|
42 def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = |
|
43 { |
|
44 Swing_Thread.assert() |
|
45 Isabelle.buffer_lock(buffer) { |
|
46 Document_Model(buffer) match { |
|
47 case Some(model) => |
|
48 val snapshot = model.snapshot() |
|
49 val markup = |
|
50 snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { |
|
51 // FIXME Isar_Document.Hyperlink extractor |
|
52 case Text.Info(info_range, |
|
53 XML.Elem(Markup(Markup.ENTITY, props), _)) |
|
54 if (props.find( |
|
55 { case (Markup.KIND, Markup.ML_OPEN) => true |
|
56 case (Markup.KIND, Markup.ML_STRUCT) => true |
|
57 case _ => false }).isEmpty) => |
|
58 val Text.Range(begin, end) = info_range |
|
59 val line = buffer.getLineOfOffset(begin) |
|
60 (Position.File.unapply(props), Position.Line.unapply(props)) match { |
|
61 case (Some(def_file), Some(def_line)) => |
|
62 new External_Hyperlink(begin, end, line, def_file, def_line) |
|
63 case _ => |
|
64 (props, props) match { |
|
65 case (Position.Id(def_id), Position.Offset(def_offset)) => |
|
66 snapshot.lookup_command(def_id) match { |
|
67 case Some(def_cmd) => |
|
68 snapshot.node.command_start(def_cmd) match { |
|
69 case Some(def_cmd_start) => |
|
70 new Internal_Hyperlink(begin, end, line, |
|
71 snapshot.convert(def_cmd_start + def_cmd.decode(def_offset))) |
|
72 case None => null |
|
73 } |
|
74 case None => null |
|
75 } |
|
76 case _ => null |
|
77 } |
|
78 } |
|
79 } |
|
80 markup match { |
|
81 case Text.Info(_, Some(link)) #:: _ => link |
|
82 case _ => null |
|
83 } |
|
84 case None => null |
|
85 } |
|
86 } |
|
87 } |
|
88 } |
|