# HG changeset patch
# User wenzelm
# Date 1468254607 -7200
# Node ID 55b1bed86c44c2dfa9891ed217b6444c7f5d390d
# Parent  19162a9ef7e361d83cf12c5101d1cabd9ba0f775
proper filter;

diff -r 19162a9ef7e3 -r 55b1bed86c44 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 18:18:24 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 18:30:07 2016 +0200
@@ -19,20 +19,20 @@
 {
   /* token navigator */
 
-  class Navigator(syntax: Outer_Syntax, buffer: Buffer, improper: Boolean)
+  class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
   {
     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
-      if (improper) it else it.filter(_.info.is_proper)
+      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 (improper) it else it.filter(_.info.is_proper)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     }
   }