tuned;
authorwenzelm
Wed, 13 Aug 2014 22:29:43 +0200
changeset 57931 4e2cbff02f23
parent 57930 3b4deb99a932
child 57932 c29659f77f8d
child 57934 5e500c0e7eca
tuned;
src/Pure/General/position.scala
src/Tools/jEdit/src/rendering.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
       }
   }
--- 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)))