approximative file position for Pure entities;
authorwenzelm
Wed, 18 Apr 2012 18:31:48 +0200
changeset 47541 4eca121e5bf5
parent 47540 1de8a8b1ae79
child 47542 26d0a76fef0a
approximative file position for Pure entities;
src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 17:32:34 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 18:31:48 2012 +0200
@@ -71,8 +71,8 @@
                   val Text.Range(begin, end) = info_range
                   val line = buffer.getLineOfOffset(begin)
                   (Position.File.unapply(props), Position.Line.unapply(props)) match {
-                    case (Some(def_file), Some(def_line)) =>
-                      new External_Hyperlink(begin, end, line, def_file, def_line)
+                    case (Some(def_file), def_line) =>
+                      new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1))
                     case _ if !snapshot.is_outdated =>
                       (props, props) match {
                         case (Position.Id(def_id), Position.Offset(def_offset)) =>