# 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)