src/Tools/jEdit/src/text_structure.scala
changeset 63440 2ce032a41a3a
parent 63439 5ad98525e918
child 63442 f6b5124b7023
equal deleted inserted replaced
63439:5ad98525e918 63440:2ce032a41a3a
    76             else if (keywords.is_command(tok, keyword_close)) - indent_size
    76             else if (keywords.is_command(tok, keyword_close)) - indent_size
    77             else 0
    77             else 0
    78 
    78 
    79           def indent_offset(tok: Token): Int =
    79           def indent_offset(tok: Token): Int =
    80             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
    80             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
       
    81             else if (tok.is_begin) indent_size
    81             else 0
    82             else 0
    82 
    83 
    83           def indent_extra: Int =
    84           def indent_extra: Int =
    84             if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
    85             if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
    85             else 0
    86             else 0
    95                     else (ind1, false)
    96                     else (ind1, false)
    96                   }
    97                   }
    97                   else (ind1, false)
    98                   else (ind1, false)
    98               }).collectFirst({ case (i, true) => i }).getOrElse(0)
    99               }).collectFirst({ case (i, true) => i }).getOrElse(0)
    99 
   100 
       
   101           def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int =
       
   102             (0 /: it)({ case (d, tok) => if (open(tok)) d + 1 else if (close(tok)) d - 1 else d })
       
   103 
       
   104           def indent_begin: Int =
       
   105             (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) *
       
   106               indent_size
       
   107 
   100           val indent =
   108           val indent =
   101             head_token(current_line) match {
   109             head_token(current_line) match {
   102               case None => indent_structure + indent_extra
   110               case None => indent_structure + indent_extra
   103               case Some(tok) =>
   111               case Some(tok) =>
   104                 if (keywords.is_command(tok, Keyword.theory)) 0
   112                 if (keywords.is_command(tok, Keyword.theory)) indent_begin
   105                 else if (tok.is_command) indent_structure - indent_offset(tok)
   113                 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
   106                 else {
   114                 else {
   107                   prev_command match {
   115                   prev_command match {
   108                     case None =>
   116                     case None =>
   109                       val extra =
   117                       val extra =
   110                         (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
   118                         (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
   111                           case (true, true) | (false, false) => 0
   119                           case (true, true) | (false, false) => 0
   112                           case (true, false) => - indent_extra
   120                           case (true, false) => - indent_extra
   113                           case (false, true) => indent_extra
   121                           case (false, true) => indent_extra
   114                         }
   122                         }
   115                       line_indent(prev_line) + extra
   123                       line_indent(prev_line) - indent_offset(tok) + extra
   116                     case Some(prev_tok) =>
   124                     case Some(prev_tok) =>
   117                       indent_structure - indent_offset(prev_tok) -
   125                       indent_structure - indent_offset(tok) - indent_offset(prev_tok) -
   118                       indent_indent(prev_tok) + indent_size
   126                       indent_indent(prev_tok) + indent_size
   119                   }
   127                   }
   120                }
   128                }
   121             }
   129             }
   122 
   130