tuned;
authorwenzelm
Wed Aug 13 22:29:43 2014 +0200 (2014-08-13)
changeset 579314e2cbff02f23
parent 57930 3b4deb99a932
child 57932 c29659f77f8d
child 57934 5e500c0e7eca
tuned;
src/Pure/General/position.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/position.scala	Wed Aug 13 20:43:19 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Wed Aug 13 22:29:43 2014 +0200
     1.3 @@ -63,20 +63,20 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  object Id_Offset
     1.8 +  object Id_Offset0
     1.9    {
    1.10      def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    1.11 -      (pos, pos) match {
    1.12 -        case (Id(id), Offset(offset)) => Some((id, offset))
    1.13 +      pos match {
    1.14 +        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
    1.15          case _ => None
    1.16        }
    1.17    }
    1.18  
    1.19 -  object Def_Id_Offset
    1.20 +  object Def_Id_Offset0
    1.21    {
    1.22      def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    1.23 -      (pos, pos) match {
    1.24 -        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
    1.25 +      pos match {
    1.26 +        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
    1.27          case _ => None
    1.28        }
    1.29    }
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 20:43:19 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 22:29:43 2014 +0200
     2.3 @@ -376,10 +376,8 @@
     2.4                  case Position.Def_Line_File(line, name) =>
     2.5                    val offset = Position.Def_Offset.unapply(props) getOrElse 0
     2.6                    PIDE.editor.hyperlink_source_file(name, line, offset)
     2.7 -                case Position.Def_Id_Offset(id, offset) =>
     2.8 +                case Position.Def_Id_Offset0(id, offset) =>
     2.9                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    2.10 -                case Position.Def_Id(id) =>
    2.11 -                  PIDE.editor.hyperlink_command_id(snapshot, id)
    2.12                  case _ => None
    2.13                }
    2.14              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    2.15 @@ -390,10 +388,8 @@
    2.16                  case Position.Line_File(line, name) =>
    2.17                    val offset = Position.Offset.unapply(props) getOrElse 0
    2.18                    PIDE.editor.hyperlink_source_file(name, line, offset)
    2.19 -                case Position.Id_Offset(id, offset) =>
    2.20 +                case Position.Id_Offset0(id, offset) =>
    2.21                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    2.22 -                case Position.Id(id) =>
    2.23 -                  PIDE.editor.hyperlink_command_id(snapshot, id)
    2.24                  case _ => None
    2.25                }
    2.26              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))