--- 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)))