src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
changeset 38426 2858ec7b6dd8
parent 38370 8b15d0f98962
child 38427 7066fbd315ae
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 22:48:56 2010 +0200
@@ -49,9 +49,9 @@
           case Some((command, command_start)) =>
             snapshot.state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
-                val begin = snapshot.convert(command_start + ref.start)
+                val begin = snapshot.convert(command_start + ref.range.start)
                 val line = buffer.getLineOfOffset(begin)
-                val end = snapshot.convert(command_start + ref.stop)
+                val end = snapshot.convert(command_start + ref.range.stop)
                 ref.info match {
                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)