src/Tools/jEdit/src/text_structure.scala
changeset 63445 5761bb8592dc
parent 63442 f6b5124b7023
child 63446 19162a9ef7e3
equal deleted inserted replaced
63444:8191c3e9f2d3 63445:5761bb8592dc
    17 
    17 
    18 object Text_Structure
    18 object Text_Structure
    19 {
    19 {
    20   /* token navigator */
    20   /* token navigator */
    21 
    21 
    22   class Navigator(syntax: Outer_Syntax, buffer: Buffer)
    22   class Navigator(syntax: Outer_Syntax, buffer: Buffer, improper: Boolean)
    23   {
    23   {
    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       Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
    27     {
    28         filter(_.info.is_proper)
    28       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
       
    29       if (improper) it else it.filter(_.info.is_proper)
       
    30     }
    29 
    31 
    30     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]] =
    31       Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
    33     {
    32         filter(_.info.is_proper)
    34       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
       
    35       if (improper) it else it.filter(_.info.is_proper)
       
    36     }
    33   }
    37   }
    34 
    38 
    35 
    39 
    36   /* indentation */
    40   /* indentation */
    37 
    41 
    44       actions: java.util.List[IndentAction])
    48       actions: java.util.List[IndentAction])
    45     {
    49     {
    46       Isabelle.buffer_syntax(buffer) match {
    50       Isabelle.buffer_syntax(buffer) match {
    47         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
    51         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
    48           val keywords = syntax.keywords
    52           val keywords = syntax.keywords
    49           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
    53           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
    50 
    54 
    51           def head_token(line: Int): Option[Token] =
    55           def head_token(line: Int): Option[Token] =
    52             nav.iterator(line, 1).toStream.headOption.map(_.info)
    56             nav.iterator(line, 1).toStream.headOption.map(_.info)
    53 
    57 
    54           def head_is_quasi_command(line: Int): Boolean =
    58           def head_is_quasi_command(line: Int): Boolean =
   167 
   171 
   168       Isabelle.buffer_syntax(text_area.getBuffer) match {
   172       Isabelle.buffer_syntax(text_area.getBuffer) match {
   169         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
   173         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
   170           val keywords = syntax.keywords
   174           val keywords = syntax.keywords
   171 
   175 
   172           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
   176           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
   173 
   177 
   174           def caret_iterator(): Iterator[Text.Info[Token]] =
   178           def caret_iterator(): Iterator[Text.Info[Token]] =
   175             nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
   179             nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
   176 
   180 
   177           def reverse_caret_iterator(): Iterator[Text.Info[Token]] =
   181           def reverse_caret_iterator(): Iterator[Text.Info[Token]] =