equal
deleted
inserted
replaced
280 |
280 |
281 val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context |
281 val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context |
282 val (tokens1, context1) = line_content(line_range.start, caret, context0) |
282 val (tokens1, context1) = line_content(line_range.start, caret, context0) |
283 val (tokens2, _) = line_content(caret, line_range.stop, context1) |
283 val (tokens2, _) = line_content(caret, line_range.stop, context1) |
284 |
284 |
285 if (tokens1.nonEmpty && tokens1.head.is_command) buffer.indentLine(line, true) |
285 if (tokens1.nonEmpty && tokens1.head.is_begin_or_command) |
286 |
286 buffer.indentLine(line, true) |
287 if (tokens2.isEmpty || tokens2.head.is_command) |
287 |
|
288 if (tokens2.isEmpty || tokens2.head.is_begin_or_command) |
288 JEdit_Lib.buffer_edit(buffer) { |
289 JEdit_Lib.buffer_edit(buffer) { |
289 text_area.setSelectedText("\n") |
290 text_area.setSelectedText("\n") |
290 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false) |
291 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false) |
291 } |
292 } |
292 else nl |
293 else nl |