# HG changeset patch
# User wenzelm
# Date 1407853209 -7200
# Node ID cbc55e5091a1d810c8666fcfae08d67006c59743
# Parent  8544ef75d1d862448ab37161c8410504ac0d0976
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;

diff -r 8544ef75d1d8 -r cbc55e5091a1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 12 16:10:59 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 12 16:20:09 2014 +0200
@@ -378,6 +378,8 @@
                   PIDE.editor.hyperlink_source_file(name, line, offset)
                 case Position.Def_Id_Offset(id, offset) =>
                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+                case Position.Def_Id(id) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id)
                 case _ => None
               }
             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
@@ -390,6 +392,8 @@
                   PIDE.editor.hyperlink_source_file(name, line, offset)
                 case Position.Id_Offset(id, offset) =>
                   PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+                case Position.Id(id) =>
+                  PIDE.editor.hyperlink_command_id(snapshot, id)
                 case _ => None
               }
             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))