62 case (Offset(start), _) => Some(Text.Range(start, start + 1)) |
62 case (Offset(start), _) => Some(Text.Range(start, start + 1)) |
63 case _ => None |
63 case _ => None |
64 } |
64 } |
65 } |
65 } |
66 |
66 |
67 object Id_Offset0 |
67 object Item_Id |
68 { |
68 { |
69 def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
69 def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
70 pos match { |
70 pos match { |
71 case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0)) |
71 case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0)) |
72 case _ => None |
72 case _ => None |
73 } |
73 } |
74 } |
74 } |
75 |
75 |
76 object Def_Id_Offset0 |
76 object Item_Def_Id |
77 { |
77 { |
78 def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
78 def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
79 pos match { |
79 pos match { |
80 case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0)) |
80 case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0)) |
|
81 case _ => None |
|
82 } |
|
83 } |
|
84 |
|
85 object Item_File |
|
86 { |
|
87 def unapply(pos: T): Option[(String, Int, Symbol.Offset)] = |
|
88 pos match { |
|
89 case Line_File(line, name) => |
|
90 val offset = Position.Offset.unapply(pos) getOrElse 0 |
|
91 Some((name, line, offset)) |
|
92 case _ => None |
|
93 } |
|
94 } |
|
95 |
|
96 object Item_Def_File |
|
97 { |
|
98 def unapply(pos: T): Option[(String, Int, Symbol.Offset)] = |
|
99 pos match { |
|
100 case Def_Line_File(line, name) => |
|
101 val offset = Position.Def_Offset.unapply(pos) getOrElse 0 |
|
102 Some((name, line, offset)) |
81 case _ => None |
103 case _ => None |
82 } |
104 } |
83 } |
105 } |
84 |
106 |
85 object Identified |
107 object Identified |