approximative file position for Pure entities;
authorwenzelm
Wed, 18 Apr 2012 18:31:48 +0200
changeset 484234eca121e5bf5
parent 48422 1de8a8b1ae79
child 48424 26d0a76fef0a
approximative file position for Pure entities;
src/Tools/jEdit/src/isabelle_hyperlinks.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 17:32:34 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 18:31:48 2012 +0200
     1.3 @@ -71,8 +71,8 @@
     1.4                    val Text.Range(begin, end) = info_range
     1.5                    val line = buffer.getLineOfOffset(begin)
     1.6                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
     1.7 -                    case (Some(def_file), Some(def_line)) =>
     1.8 -                      new External_Hyperlink(begin, end, line, def_file, def_line)
     1.9 +                    case (Some(def_file), def_line) =>
    1.10 +                      new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1))
    1.11                      case _ if !snapshot.is_outdated =>
    1.12                        (props, props) match {
    1.13                          case (Position.Id(def_id), Position.Offset(def_offset)) =>