# HG changeset patch
# User wenzelm
# Date 1407961783 -7200
# Node ID 4e2cbff02f2359d7983510602b75438c43464d18
# Parent  3b4deb99a932ecb7ecf0bd21a845be1a0949ef7d
tuned;

diff -r 3b4deb99a932 -r 4e2cbff02f23 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed Aug 13 20:43:19 2014 +0200
+++ b/src/Pure/General/position.scala	Wed Aug 13 22:29:43 2014 +0200
@@ -63,20 +63,20 @@
       }
   }
 
-  object Id_Offset
+  object Id_Offset0
   {
     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
-      (pos, pos) match {
-        case (Id(id), Offset(offset)) => Some((id, offset))
+      pos match {
+        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
         case _ => None
       }
   }
 
-  object Def_Id_Offset
+  object Def_Id_Offset0
   {
     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
-      (pos, pos) match {
-        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
+      pos match {
+        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
         case _ => None
       }
   }
diff -r 3b4deb99a932 -r 4e2cbff02f23 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 20:43:19 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 22:29:43 2014 +0200
@@ -376,10 +376,8 @@
                 case Position.Def_Line_File(line, name) =>
                   val offset = Position.Def_Offset.unapply(props) getOrElse 0
                   PIDE.editor.hyperlink_source_file(name, line, offset)
-                case Position.Def_Id_Offset(id, offset) =>
+                case Position.Def_Id_Offset0(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,10 +388,8 @@
                 case Position.Line_File(line, name) =>
                   val offset = Position.Offset.unapply(props) getOrElse 0
                   PIDE.editor.hyperlink_source_file(name, line, offset)
-                case Position.Id_Offset(id, offset) =>
+                case Position.Id_Offset0(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)))