Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
authorwenzelm
Tue, 12 Aug 2014 16:20:09 +0200
changeset 57914 cbc55e5091a1
parent 57913 8544ef75d1d8
child 57915 448325de6e4f
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
src/Tools/jEdit/src/rendering.scala file | annotate | diff | comparison | revisions 
--- 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)))
isabelle