include trailing comments in proper_command range;
authorwenzelm
Fri, 13 Apr 2012 21:17:59 +0200
changeset 47459 373e456149cc
parent 47458 29b3f9cba73d
child 47460 70fd47ca62e3
include trailing comments in proper_command range;
src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Apr 13 21:09:11 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Apr 13 21:17:59 2012 +0200
@@ -145,7 +145,7 @@
   val range: Text.Range = Text.Range(0, length)
 
   val proper_range: Text.Range =
-    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
+    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_space))(_ - _.source.length))
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)