1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -49,9 +49,9 @@
     1.4            case Some((command, command_start)) =>
     1.5              snapshot.state(command).ref_at(offset - command_start) match {
     1.6                case Some(ref) =>
     1.7 -                val begin = snapshot.convert(command_start + ref.start)
     1.8 +                val begin = snapshot.convert(command_start + ref.range.start)
     1.9                  val line = buffer.getLineOfOffset(begin)
    1.10 -                val end = snapshot.convert(command_start + ref.stop)
    1.11 +                val end = snapshot.convert(command_start + ref.range.stop)
    1.12                  ref.info match {
    1.13                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    1.14                      new External_Hyperlink(begin, end, line, ref_file, ref_line)