# HG changeset patch
# User wenzelm
# Date 1334344679 -7200
# Node ID 373e456149ccdf41e12090f91a2b0ea53bd2ffae
# Parent  29b3f9cba73d0a07940e96e45ad6cb4753aa8e54
include trailing comments in proper_command range;

diff -r 29b3f9cba73d -r 373e456149cc 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)