src/Pure/PIDE/command.scala
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)