# HG changeset patch
# User wenzelm
# Date 1503321784 -7200
# Node ID a6ec0172211aa889c897843f8dcb41c838f92f65
# Parent  075c2aadd0b847c329ee5aa33aa5847ef7a255a8
avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";

diff -r 075c2aadd0b8 -r a6ec0172211a src/Tools/jEdit/src/isabelle.scala
--- 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
         }