equal
deleted
inserted
replaced
69 } |
69 } |
70 |
70 |
71 val prev_line: Int = |
71 val prev_line: Int = |
72 Range.inclusive(current_line - 1, 0, -1).find(line => |
72 Range.inclusive(current_line - 1, 0, -1).find(line => |
73 Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && |
73 Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && |
74 !Token_Markup.Line_Context.after(buffer, line).structure.improper) getOrElse -1 |
74 (!Token_Markup.Line_Context.after(buffer, line).structure.improper || |
|
75 Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 |
75 |
76 |
76 def prev_line_command: Option[Token] = |
77 def prev_line_command: Option[Token] = |
77 nav.reverse_iterator(prev_line, 1). |
78 nav.reverse_iterator(prev_line, 1). |
78 collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) |
79 collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) |
79 |
80 |