# HG changeset patch
# User wenzelm
# Date 1473166942 -7200
# Node ID 56670ab6f55e3f23171cbf8d241f50cf6064d86d
# Parent  e8462a4349fcd84c382a68c1cd4af769c3deeb0d
tuned;

diff -r e8462a4349fc -r 56670ab6f55e src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Tue Sep 06 13:26:14 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Tue Sep 06 15:02:22 2016 +0200
@@ -183,6 +183,9 @@
     def is_quasi_command(token: Token): Boolean =
       token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
 
+    def is_indent_command(token: Token): Boolean =
+      token.is_begin_or_command || is_quasi_command(token)
+
 
     /* load commands */
 
diff -r e8462a4349fc -r 56670ab6f55e src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 06 13:26:14 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Sep 06 15:02:22 2016 +0200
@@ -284,12 +284,10 @@
             val (tokens1, context1) = line_content(line_range.start, caret, context0)
             val (tokens2, _) = line_content(caret, line_range.stop, context1)
 
-            if (tokens1.nonEmpty &&
-                (tokens1.head.is_begin_or_command || keywords.is_quasi_command(tokens1.head)))
+            if (tokens1.nonEmpty && keywords.is_indent_command(tokens1.head))
               buffer.indentLine(line, true)
 
-            if (tokens2.isEmpty ||
-                tokens2.head.is_begin_or_command || keywords.is_quasi_command(tokens2.head))
+            if (tokens2.isEmpty || keywords.is_indent_command(tokens2.head))
               JEdit_Lib.buffer_edit(buffer) {
                 text_area.setSelectedText("\n")
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)