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