avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
--- a/src/Tools/jEdit/src/isabelle.scala Mon Aug 21 11:36:34 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Aug 21 15:23:04 2017 +0200
@@ -290,11 +290,10 @@
if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)
- if (toks2.isEmpty || keywords.is_indent_command(toks2.head))
- JEdit_Lib.buffer_edit(buffer) {
- text_area.setSelectedText("\n")
- if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
- }
+ if (toks2.isEmpty || keywords.is_indent_command(toks2.head)) {
+ text_area.setSelectedText("\n")
+ if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
+ }
else nl
case None => nl
}