# HG changeset patch
# User wenzelm
# Date 1468433656 -7200
# Node ID 2033a3960c36249f5f15094f4458219551fa0323
# Parent  2c9444125485bae292fb3beacf839fe0828f4a1a
auto indentation of quasi commands;

diff -r 2c9444125485 -r 2033a3960c36 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 13 20:04:57 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 13 20:14:16 2016 +0200
@@ -265,6 +265,8 @@
       {
         Isabelle.buffer_syntax(buffer) match {
           case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+            val keywords = syntax.keywords
+
             val caret = text_area.getCaretPosition
             val line = text_area.getCaretLine
             val line_range = JEdit_Lib.line_range(buffer, line)
@@ -282,10 +284,12 @@
             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)
+            if (tokens1.nonEmpty &&
+                (tokens1.head.is_begin_or_command || keywords.is_quasi_command(tokens1.head)))
               buffer.indentLine(line, true)
 
-            if (tokens2.isEmpty || tokens2.head.is_begin_or_command)
+            if (tokens2.isEmpty ||
+                tokens2.head.is_begin_or_command || keywords.is_quasi_command(tokens2.head))
               JEdit_Lib.buffer_edit(buffer) {
                 text_area.setSelectedText("\n")
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)