author | wenzelm |
Tue, 08 Dec 2009 14:49:01 +0100 | |
changeset 34759 | bfea7839d9e1 |
parent 34714 | src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala@983becb5ae9a |
child 34760 | dc7f5e0d9d27 |
permissions | -rw-r--r-- |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
1 |
/* |
34588 | 2 |
* Hyperlink setup for Isabelle proof documents |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
3 |
* |
34588 | 4 |
* @author Fabian Immler, TU Munich |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
5 |
*/ |
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 |
|
9 |
import java.io.File |
|
10 |
||
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
11 |
import gatchan.jedit.hyperlinks.Hyperlink |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
12 |
import gatchan.jedit.hyperlinks.HyperlinkSource |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
13 |
import gatchan.jedit.hyperlinks.AbstractHyperlink |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
14 |
|
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.View |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
16 |
import org.gjt.sp.jedit.jEdit |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.Buffer |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
18 |
import org.gjt.sp.jedit.TextUtilities |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
19 |
|
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34704
diff
changeset
|
20 |
import isabelle.prover.Command |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
21 |
|
34588 | 22 |
|
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
23 |
class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int) |
34569 | 24 |
extends AbstractHyperlink(start, end, line, "") |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
25 |
{ |
34582 | 26 |
override def click(view: View) { |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
27 |
view.getTextArea.moveCaretPosition(ref_offset) |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
28 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
29 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
30 |
|
34569 | 31 |
class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int) |
32 |
extends AbstractHyperlink(start, end, line, "") |
|
33 |
{ |
|
34602
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
34 |
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
|
35 |
Isabelle.system.source_file(ref_file) match { |
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
36 |
case None => System.err.println("Could not find source file " + ref_file) |
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
37 |
case Some(file) => |
34573 | 38 |
jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) |
39 |
} |
|
34602
782b1948aca9
ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents:
34588
diff
changeset
|
40 |
} |
34569 | 41 |
} |
42 |
||
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
43 |
class IsabelleHyperlinkSource extends HyperlinkSource |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
44 |
{ |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
45 |
def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
46 |
val prover = Isabelle.prover_setup(buffer).map(_.prover) |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
47 |
val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view) |
34714 | 48 |
if (prover.isEmpty || theory_view_opt.isEmpty) null |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
49 |
else if (prover.get == null || theory_view_opt.get == null) null |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
50 |
else { |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
51 |
val theory_view = theory_view_opt.get |
34650 | 52 |
val document = theory_view.current_document() |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
53 |
val offset = theory_view.from_current(document, original_offset) |
34712
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
54 |
document.command_at(offset) match { |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
55 |
case Some(command) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
56 |
command.ref_at(document, offset - command.start(document)) match { |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
57 |
case Some(ref) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
58 |
val command_start = command.start(document) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
59 |
val begin = theory_view.to_current(document, command_start + ref.start) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
60 |
val line = buffer.getLineOfOffset(begin) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
61 |
val end = theory_view.to_current(document, command_start + ref.stop) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
62 |
ref.info match { |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
63 |
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
64 |
new ExternalHyperlink(begin, end, line, ref_file, ref_line) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
65 |
case Command.RefInfo(_, _, Some(id), Some(offset)) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
66 |
prover.get.command(id) match { |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
67 |
case Some(ref_cmd) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
68 |
new InternalHyperlink(begin, end, line, |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
69 |
theory_view.to_current(document, ref_cmd.start(document) + offset - 1)) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
70 |
case None => null |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
71 |
} |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
72 |
case _ => null |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
73 |
} |
34712
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
74 |
case None => null |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
75 |
} |
34712
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
76 |
case None => null |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34707
diff
changeset
|
77 |
} |
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
78 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
79 |
} |
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff
changeset
|
80 |
} |