src/Tools/jEdit/src/rendering.scala
changeset 57931 4e2cbff02f23
parent 57914 cbc55e5091a1
child 58048 aa6296d09e0e
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 20:43:19 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 13 22:29:43 2014 +0200
     1.3 @@ -376,10 +376,8 @@
     1.4                  case Position.Def_Line_File(line, name) =>
     1.5                    val offset = Position.Def_Offset.unapply(props) getOrElse 0
     1.6                    PIDE.editor.hyperlink_source_file(name, line, offset)
     1.7 -                case Position.Def_Id_Offset(id, offset) =>
     1.8 +                case Position.Def_Id_Offset0(id, offset) =>
     1.9                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.10 -                case Position.Def_Id(id) =>
    1.11 -                  PIDE.editor.hyperlink_command_id(snapshot, id)
    1.12                  case _ => None
    1.13                }
    1.14              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.15 @@ -390,10 +388,8 @@
    1.16                  case Position.Line_File(line, name) =>
    1.17                    val offset = Position.Offset.unapply(props) getOrElse 0
    1.18                    PIDE.editor.hyperlink_source_file(name, line, offset)
    1.19 -                case Position.Id_Offset(id, offset) =>
    1.20 +                case Position.Id_Offset0(id, offset) =>
    1.21                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.22 -                case Position.Id(id) =>
    1.23 -                  PIDE.editor.hyperlink_command_id(snapshot, id)
    1.24                  case _ => None
    1.25                }
    1.26              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))