--- 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)