more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
authorwenzelm
Sun Dec 04 13:47:56 2016 +0100 (2016-12-04)
changeset 64536e61de633a3ed
parent 64535 4f161e8cdaac
child 64537 693389d87139
child 64547 a955511171a8
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/Tools/jEdit/src/text_structure.scala	Sun Dec 04 13:40:54 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Sun Dec 04 13:47:56 2016 +0100
     1.3 @@ -142,7 +142,6 @@
     1.4            val indent =
     1.5              if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
     1.6                line_head(current_line) match {
     1.7 -                case None => indent_structure + indent_brackets + indent_extra
     1.8                  case Some(info @ Text.Info(range, tok)) =>
     1.9                    if (tok.is_begin ||
    1.10                        keywords.is_before_command(tok) ||
    1.11 @@ -166,7 +165,16 @@
    1.12                          indent_structure + indent_brackets + indent_size - indent_offset(tok) -
    1.13                          indent_offset(prev_tok) - indent_indent(prev_tok)
    1.14                      }
    1.15 -                 }
    1.16 +                  }
    1.17 +                case None =>
    1.18 +                  prev_line_command match {
    1.19 +                    case None =>
    1.20 +                      val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
    1.21 +                      line_indent(prev_line) + indent_brackets + extra
    1.22 +                    case Some(prev_tok) =>
    1.23 +                      indent_structure + indent_brackets + indent_size -
    1.24 +                      indent_offset(prev_tok) - indent_indent(prev_tok)
    1.25 +                  }
    1.26                }
    1.27              }
    1.28              else line_indent(current_line)