--- a/src/Pure/PIDE/command.scala Fri Aug 24 16:45:55 2012 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 24 19:35:44 2012 +0200
@@ -153,10 +153,6 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- val newlines =
- (0 /: Symbol.iterator(source)) {
- case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
-
lazy val symbol_index = new Symbol.Index(source)
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)