more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');

--- a/src/Tools/jEdit/src/text_structure.scala	Sun Dec 04 13:40:54 2016 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Sun Dec 04 13:47:56 2016 +0100
@@ -142,7 +142,6 @@
           val indent =
             if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
               line_head(current_line) match {
-                case None => indent_structure + indent_brackets + indent_extra
                 case Some(info @ Text.Info(range, tok)) =>
                   if (tok.is_begin ||
                       keywords.is_before_command(tok) ||
@@ -166,7 +165,16 @@
                         indent_structure + indent_brackets + indent_size - indent_offset(tok) -
                         indent_offset(prev_tok) - indent_indent(prev_tok)
                     }
-                 }
+                  }
+                case None =>
+                  prev_line_command match {
+                    case None =>
+                      val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
+                      line_indent(prev_line) + indent_brackets + extra
+                    case Some(prev_tok) =>
+                      indent_structure + indent_brackets + indent_size -
+                      indent_offset(prev_tok) - indent_indent(prev_tok)
+                  }
               }
             }
             else line_indent(current_line)