--- a/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 14:59:00 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 15:46:25 2017 +0200
@@ -71,7 +71,8 @@
val prev_line: Int =
Range.inclusive(current_line - 1, 0, -1).find(line =>
Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished &&
- !Token_Markup.Line_Context.after(buffer, line).structure.improper) getOrElse -1
+ (!Token_Markup.Line_Context.after(buffer, line).structure.improper ||
+ Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1
def prev_line_command: Option[Token] =
nav.reverse_iterator(prev_line, 1).