src/Tools/jEdit/src/text_structure.scala
changeset 68730 0bc491938780
parent 67014 e6a695d6a6b2
     1.1 --- a/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:11:24 2018 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:21:20 2018 +0200
     1.3 @@ -26,13 +26,13 @@
     1.4      def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     1.5      {
     1.6        val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
     1.7 -      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
     1.8 +      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     1.9      }
    1.10  
    1.11      def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    1.12      {
    1.13        val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
    1.14 -      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    1.15 +      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
    1.16      }
    1.17    }
    1.18