# HG changeset patch
# User wenzelm
# Date 1283191881 -7200
# Node ID 682c4932b3cca83b3e4b5309a45232e4d621eacc
# Parent  ec7045139e7023f5878a027de87aadb8bd118aa5
Command.newlines: account for physical newlines;

diff -r ec7045139e70 -r 682c4932b3cc src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Aug 30 16:49:41 2010 +0200
+++ b/src/Pure/General/symbol.scala	Mon Aug 30 20:11:21 2010 +0200
@@ -53,6 +53,9 @@
 
   def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
+  def is_physical_newline(s: CharSequence): Boolean =
+    "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+
   def is_wellformed(s: CharSequence): Boolean =
     s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
 
diff -r ec7045139e70 -r 682c4932b3cc src/Pure/PIDE/command.scala
--- 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)