clarified prev_line: stop at blank line;
authorwenzelm
Fri, 23 Jun 2017 15:46:25 +0200
changeset 66178 5f02bf37324f
parent 66177 7fd83f20e3e9
child 66179 148d61626014
clarified prev_line: stop at blank line;
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).