# HG changeset patch
# User wenzelm
# Date 1498225585 -7200
# Node ID 5f02bf37324f4db9b9387f4ee6062b401e05f9d0
# Parent  7fd83f20e3e914deaacc8142439613bd717ccae4
clarified prev_line: stop at blank line;

diff -r 7fd83f20e3e9 -r 5f02bf37324f src/Tools/jEdit/src/text_structure.scala
--- 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).