--- a/src/Tools/jEdit/src/text_structure.scala Tue Jul 31 21:11:24 2018 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Tue Jul 31 21:21:20 2018 +0200
@@ -26,13 +26,13 @@
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
{
val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
- if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+ if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
}
def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
{
val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
- if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+ if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
}
}