--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 15 19:50:55 2009 +0100
@@ -45,18 +45,18 @@
{
def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
{
- Isabelle.plugin.theory_view(buffer) match {
- case Some(theory_view) =>
- val document = theory_view.current_document()
- val offset = theory_view.from_current(document, original_offset)
+ Document_Model.get(buffer) match {
+ case Some(model) =>
+ val document = model.current_document()
+ val offset = model.from_current(document, original_offset)
document.command_at(offset) match {
case Some(command) =>
command.ref_at(document, offset - command.start(document)) match {
case Some(ref) =>
val command_start = command.start(document)
- val begin = theory_view.to_current(document, command_start + ref.start)
+ val begin = model.to_current(document, command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
- val end = theory_view.to_current(document, command_start + ref.stop)
+ val end = model.to_current(document, command_start + ref.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
@@ -64,7 +64,7 @@
Isabelle.session.command(id) match {
case Some(ref_cmd) =>
new Internal_Hyperlink(begin, end, line,
- theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+ model.to_current(document, ref_cmd.start(document) + offset - 1))
case None => null
}
case _ => null