# HG changeset patch
# User wenzelm
# Date 1334766708 -7200
# Node ID 4eca121e5bf5431080babdbdbd8026124178eb34
# Parent  1de8a8b1ae7959d1c0b7c76e222d44257d3ccb33
approximative file position for Pure entities;

diff -r 1de8a8b1ae79 -r 4eca121e5bf5 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)) =>