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