skip over inner syntax for indentation;
authorwenzelm
Mon Nov 21 14:49:52 2016 +0100 (2016-11-21)
changeset 64518b87697eec2ac
parent 64517 62832c7df18f
child 64519 51be997d0698
skip over inner syntax for indentation;
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/Tools/jEdit/src/text_structure.scala	Mon Nov 21 14:47:15 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Mon Nov 21 14:49:52 2016 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4      private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
     1.5      private val keyword_close = Keyword.proof_close
     1.6  
     1.7 -    def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int,
     1.8 +    def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
     1.9        actions: java.util.List[IndentAction])
    1.10      {
    1.11        Isabelle.buffer_syntax(buffer) match {
    1.12 @@ -68,6 +68,11 @@
    1.13                case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
    1.14              }
    1.15  
    1.16 +          val prev_line: Int =
    1.17 +            Range.inclusive(current_line - 1, 0, -1).find(line =>
    1.18 +              Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
    1.19 +              !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
    1.20 +
    1.21            def prev_line_command: Option[Token] =
    1.22              nav.reverse_iterator(prev_line, 1).
    1.23                collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
    1.24 @@ -135,33 +140,36 @@
    1.25              else 0
    1.26  
    1.27            val indent =
    1.28 -            line_head(current_line) match {
    1.29 -              case None => indent_structure + indent_brackets + indent_extra
    1.30 -              case Some(info @ Text.Info(range, tok)) =>
    1.31 -                if (tok.is_begin ||
    1.32 -                    keywords.is_before_command(tok) ||
    1.33 -                    keywords.is_command(tok, Keyword.theory)) 0
    1.34 -                else if (keywords.is_command(tok, Keyword.proof_enclose))
    1.35 -                  indent_structure + script_indent(info) - indent_offset(tok)
    1.36 -                else if (keywords.is_command(tok, Keyword.proof))
    1.37 -                  (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
    1.38 -                else if (tok.is_command) indent_structure - indent_offset(tok)
    1.39 -                else {
    1.40 -                  prev_line_command match {
    1.41 -                    case None =>
    1.42 -                      val extra =
    1.43 -                        (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
    1.44 -                          case (true, true) | (false, false) => 0
    1.45 -                          case (true, false) => - indent_extra
    1.46 -                          case (false, true) => indent_extra
    1.47 -                        }
    1.48 -                      line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
    1.49 -                    case Some(prev_tok) =>
    1.50 -                      indent_structure + indent_brackets + indent_size - indent_offset(tok) -
    1.51 -                      indent_offset(prev_tok) - indent_indent(prev_tok)
    1.52 -                  }
    1.53 -               }
    1.54 +            if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
    1.55 +              line_head(current_line) match {
    1.56 +                case None => indent_structure + indent_brackets + indent_extra
    1.57 +                case Some(info @ Text.Info(range, tok)) =>
    1.58 +                  if (tok.is_begin ||
    1.59 +                      keywords.is_before_command(tok) ||
    1.60 +                      keywords.is_command(tok, Keyword.theory)) 0
    1.61 +                  else if (keywords.is_command(tok, Keyword.proof_enclose))
    1.62 +                    indent_structure + script_indent(info) - indent_offset(tok)
    1.63 +                  else if (keywords.is_command(tok, Keyword.proof))
    1.64 +                    (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
    1.65 +                  else if (tok.is_command) indent_structure - indent_offset(tok)
    1.66 +                  else {
    1.67 +                    prev_line_command match {
    1.68 +                      case None =>
    1.69 +                        val extra =
    1.70 +                          (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
    1.71 +                            case (true, true) | (false, false) => 0
    1.72 +                            case (true, false) => - indent_extra
    1.73 +                            case (false, true) => indent_extra
    1.74 +                          }
    1.75 +                        line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
    1.76 +                      case Some(prev_tok) =>
    1.77 +                        indent_structure + indent_brackets + indent_size - indent_offset(tok) -
    1.78 +                        indent_offset(prev_tok) - indent_indent(prev_tok)
    1.79 +                    }
    1.80 +                 }
    1.81 +              }
    1.82              }
    1.83 +            else line_indent(current_line)
    1.84  
    1.85            actions.clear()
    1.86            actions.add(new IndentAction.AlignOffset(indent max 0))