proper filter;

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