1.1 --- a/src/Pure/PIDE/command.scala	Fri Apr 13 21:09:11 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Apr 13 21:17:59 2012 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4    val range: Text.Range = Text.Range(0, length)
     1.5  
     1.6    val proper_range: Text.Range =
     1.7 -    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
     1.8 +    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length))
     1.9  
    1.10    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.11