src/Tools/jEdit/src/text_structure.scala
changeset 68730 0bc491938780
parent 67014 e6a695d6a6b2
child 71601 97ccf48c2f0c
equal deleted inserted replaced
68729:3a02b424d5fb 68730:0bc491938780
    24     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
    24     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
    25 
    25 
    26     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    26     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    27     {
    27     {
    28       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
    28       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
    29       if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    29       if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
    30     }
    30     }
    31 
    31 
    32     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    32     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    33     {
    33     {
    34       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
    34       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
    35       if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    35       if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
    36     }
    36     }
    37   }
    37   }
    38 
    38 
    39 
    39 
    40   /* indentation */
    40   /* indentation */