equal
deleted
inserted
replaced
73 case (Def_Id(id), Def_Offset(offset)) => Some((id, offset)) |
73 case (Def_Id(id), Def_Offset(offset)) => Some((id, offset)) |
74 case _ => None |
74 case _ => None |
75 } |
75 } |
76 } |
76 } |
77 |
77 |
78 object Id_Range |
78 object Reported |
79 { |
79 { |
80 def unapply(pos: T): Option[(Long, Text.Range)] = |
80 def unapply(pos: T): Option[(Long, String, Text.Range)] = |
81 (pos, pos) match { |
81 (pos, pos) match { |
82 case (Id(id), Range(range)) => Some((id, range)) |
82 case (Id(id), Range(range)) => |
|
83 Some((id, File.unapply(pos).getOrElse(""), range)) |
83 case _ => None |
84 case _ => None |
84 } |
85 } |
85 } |
86 } |
86 |
87 |
87 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
88 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |