equal
deleted
inserted
replaced
207 |
207 |
208 def length: Int = source.length |
208 def length: Int = source.length |
209 val range: Text.Range = Text.Range(0, length) |
209 val range: Text.Range = Text.Range(0, length) |
210 |
210 |
211 val proper_range: Text.Range = |
211 val proper_range: Text.Range = |
212 Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length)) |
212 Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) |
213 |
213 |
214 def source(range: Text.Range): String = source.substring(range.start, range.stop) |
214 def source(range: Text.Range): String = source.substring(range.start, range.stop) |
215 |
215 |
216 lazy val symbol_index = new Symbol.Index(source) |
216 lazy val symbol_index = new Symbol.Index(source) |
217 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
217 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |