author | wenzelm |
Sun, 22 Aug 2010 19:55:41 +0200 | |
changeset 38580 | 881c362d48e4 |
parent 38577 | 4e4d3ea3725a |
child 38582 | 3a6ce43d99b1 |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/isabelle_hyperlinks.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
||
4 |
Hyperlink setup for Isabelle proof documents. |
|
5 |
*/ |
|
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
6 |
|
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
7 |
package isabelle.jedit |
34569 | 8 |
|
34760 | 9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
34569 | 12 |
import java.io.File |
13 |
||
34791 | 14 |
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink} |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
15 |
|
34791 | 16 |
import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities} |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
17 |
|
34588 | 18 |
|
34760 | 19 |
private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int) |
34569 | 20 |
extends AbstractHyperlink(start, end, line, "") |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
21 |
{ |
34582 | 22 |
override def click(view: View) { |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
23 |
view.getTextArea.moveCaretPosition(ref_offset) |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
24 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
25 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
26 |
|
34760 | 27 |
class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int) |
34569 | 28 |
extends AbstractHyperlink(start, end, line, "") |
29 |
{ |
|
34602
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
30 |
override def click(view: View) = { |
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
31 |
Isabelle.system.source_file(ref_file) match { |
34760 | 32 |
case None => System.err.println("Could not find source file " + ref_file) // FIXME ?? |
34602
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
33 |
case Some(file) => |
34573 | 34 |
jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
35 |
} |
|
34602
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
36 |
} |
34569 | 37 |
} |
38 |
||
34760 | 39 |
class Isabelle_Hyperlinks extends HyperlinkSource |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
40 |
{ |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
41 |
def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = |
37175 | 42 |
{ |
38223 | 43 |
Swing_Thread.assert() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
44 |
Document_Model(buffer) match { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
45 |
case Some(model) => |
38151 | 46 |
val snapshot = model.snapshot() |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
47 |
val offset = snapshot.revert(buffer_offset) |
38152
eab0d1c2e46e
Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents:
38151
diff
changeset
|
48 |
snapshot.node.command_at(offset) match { |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34832
diff
changeset
|
49 |
case Some((command, command_start)) => |
38577 | 50 |
val root = Text.Info[Hyperlink]((Text.Range(offset) - command_start), null) |
51 |
(snapshot.state(command).markup.select(root) { |
|
38580
881c362d48e4
proper range for hyperlinks and tooltips, using original markup information;
wenzelm
parents:
38577
diff
changeset
|
52 |
case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), |
38577 | 53 |
List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => |
54 |
val Text.Range(begin, end) = snapshot.convert(info_range + command_start) |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
55 |
val line = buffer.getLineOfOffset(begin) |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
56 |
|
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
57 |
(Position.get_file(props), Position.get_line(props)) match { |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
58 |
case (Some(ref_file), Some(ref_line)) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
59 |
new External_Hyperlink(begin, end, line, ref_file, ref_line) |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
60 |
case _ => |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
61 |
(Position.get_id(props), Position.get_offset(props)) match { |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
62 |
case (Some(ref_id), Some(ref_offset)) => |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
63 |
snapshot.lookup_command(ref_id) match { |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
64 |
case Some(ref_cmd) => |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
65 |
snapshot.node.command_start(ref_cmd) match { |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
66 |
case Some(ref_cmd_start) => |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
67 |
new Internal_Hyperlink(begin, end, line, |
38580
881c362d48e4
proper range for hyperlinks and tooltips, using original markup information;
wenzelm
parents:
38577
diff
changeset
|
68 |
snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset))) |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
69 |
case None => null |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
70 |
} |
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
71 |
case None => null |
34858 | 72 |
} |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34791
diff
changeset
|
73 |
case _ => null |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
74 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
75 |
} |
38575
80d962964216
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents:
38427
diff
changeset
|
76 |
}).head.info |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
77 |
case None => null |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
78 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
79 |
case None => null |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
80 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
81 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
82 |
} |