1.1 --- a/src/Pure/General/symbol.scala	Mon Aug 30 16:49:41 2010 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Aug 30 20:11:21 2010 +0200
     1.3 @@ -53,6 +53,9 @@
     1.4  
     1.5    def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
     1.6  
     1.7 +  def is_physical_newline(s: CharSequence): Boolean =
     1.8 +    "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
     1.9 +
    1.10    def is_wellformed(s: CharSequence): Boolean =
    1.11      s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
    1.12  

     2.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 30 16:49:41 2010 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 30 20:11:21 2010 +0200
     2.3 @@ -96,6 +96,10 @@
     2.4    def source(range: Text.Range): String = source.substring(range.start, range.stop)
     2.5    def length: Int = source.length
     2.6  
     2.7 +  val newlines =
     2.8 +    (0 /: Symbol.iterator(source)) {
     2.9 +      case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
    2.10 +
    2.11    val range: Text.Range = Text.Range(0, length)
    2.12  
    2.13    lazy val symbol_index = new Symbol.Index(source)