changeset 38877 | 682c4932b3cc |
parent 38872 | 26c505765024 |
child 38887 | 1261481ef5e5 |
--- a/src/Pure/PIDE/command.scala Mon Aug 30 16:49:41 2010 +0200 +++ b/src/Pure/PIDE/command.scala Mon Aug 30 20:11:21 2010 +0200 @@ -96,6 +96,10 @@ def source(range: Text.Range): String = source.substring(range.start, range.stop) def length: Int = source.length + val newlines = + (0 /: Symbol.iterator(source)) { + case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n } + val range: Text.Range = Text.Range(0, length) lazy val symbol_index = new Symbol.Index(source)