--- a/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 15:46:25 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 16:16:41 2017 +0200
@@ -141,8 +141,10 @@
else 0
val indent =
- if (Token_Markup.Line_Context.before(buffer, current_line).get_context == Scan.Finished)
- {
+ if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished)
+ line_indent(current_line)
+ else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
+ else {
line_head(current_line) match {
case Some(info @ Text.Info(range, tok)) =>
if (tok.is_begin ||
@@ -179,7 +181,6 @@
}
}
}
- else line_indent(current_line)
actions.clear()
actions.add(new IndentAction.AlignOffset(indent max 0))