--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Jan 10 17:10:32 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Jan 10 20:14:21 2010 +0100
@@ -44,10 +44,9 @@
val document = model.recent_document()
val offset = model.from_current(document, original_offset)
document.command_at(offset) match {
- case Some(command) =>
- document.current_state(command).ref_at(offset - command.start(document)) match {
+ case Some((command, command_start)) =>
+ document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
- val command_start = command.start(document)
val begin = model.to_current(document, command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
val end = model.to_current(document, command_start + ref.stop)