equal
deleted
inserted
replaced
82 sealed case class Node_Position(name: String, pos: Position = Position.zero) { |
82 sealed case class Node_Position(name: String, pos: Position = Position.zero) { |
83 def line: Int = pos.line |
83 def line: Int = pos.line |
84 def line1: Int = pos.line1 |
84 def line1: Int = pos.line1 |
85 def column: Int = pos.column |
85 def column: Int = pos.column |
86 def column1: Int = pos.column1 |
86 def column1: Int = pos.column1 |
|
87 |
|
88 def advance(text: String): Node_Position = |
|
89 if (text.isEmpty) this |
|
90 else copy(pos = pos.advance(text)) |
87 } |
91 } |
88 |
92 |
89 sealed case class Node_Range(name: String, range: Range = Range.zero) { |
93 sealed case class Node_Range(name: String, range: Range = Range.zero) { |
90 def start: Position = range.start |
94 def start: Position = range.start |
91 def stop: Position = range.stop |
95 def stop: Position = range.stop |