indentation of keywords after input;

--- a/src/Tools/jEdit/etc/options	Fri Jun 23 16:16:41 2017 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Jun 23 22:03:51 2017 +0200
@@ -39,6 +39,9 @@
 
 section "Indentation"
 
+public option jedit_indent_input : bool = true
+  -- "indentation of Isabelle keywords after input (typed character or completion)"
+
 public option jedit_indent_newline : bool = true
   -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)"
 

--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 23 16:16:41 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 23 22:03:51 2017 +0200
@@ -218,6 +218,7 @@
                   buffer.remove(range.start, range.length)
                   buffer.insert(range.start, item.replacement)
                   text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
+                  Isabelle.indent_input(text_area)
               }
             case _ =>
           }
@@ -346,11 +347,13 @@
     {
       GUI_Thread.require {}
 
-      if (PIDE.options.bool("jedit_completion")) {
-        if (!evt.isConsumed) {
+      if (!evt.isConsumed) {
+        val backspace = evt.getKeyChar == '\b'
+        val special = JEdit_Lib.special_key(evt)
+
+        if (PIDE.options.bool("jedit_completion")) {
           dismissed()
-          if (evt.getKeyChar != '\b') {
-            val special = JEdit_Lib.special_key(evt)
+          if (!backspace) {
             val immediate = PIDE.options.bool("jedit_completion_immediate")
             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
               input_delay.revoke()
@@ -364,6 +367,8 @@
             }
           }
         }
+
+        if (!backspace && !special) Isabelle.indent_input(text_area)
       }
     }
 

--- a/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 16:16:41 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 22:03:51 2017 +0200
@@ -244,6 +244,32 @@
 
   /* structured edits */
 
+  def indent_enabled(buffer: JEditBuffer, option: String): Boolean =
+    indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
+    buffer.getStringProperty("autoIndent") == "full" &&
+    PIDE.options.bool(option)
+
+  def indent_input(text_area: TextArea)
+  {
+    val buffer = text_area.getBuffer
+    val line = text_area.getCaretLine
+    val caret = text_area.getCaretPosition
+
+    if (text_area.isEditable && indent_enabled(buffer, "jedit_indent_input")) {
+      buffer_syntax(buffer) match {
+        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+          val nav = new Text_Structure.Navigator(syntax, buffer.asInstanceOf[Buffer], true)
+          nav.iterator(line, 1).toStream.headOption match {
+            case Some(Text.Info(range, tok))
+            if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
+              buffer.indentLine(line, true)
+            case _ =>
+          }
+        case _ =>
+      }
+    }
+  }
+
   def newline(text_area: TextArea)
   {
     if (!text_area.isEditable()) text_area.getToolkit().beep()
@@ -251,11 +277,8 @@
       val buffer = text_area.getBuffer
       def nl { text_area.userInput('\n') }
 
-      if (indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
-          buffer.getStringProperty("autoIndent") == "full" &&
-          PIDE.options.bool("jedit_indent_newline"))
-      {
-        Isabelle.buffer_syntax(buffer) match {
+      if (indent_enabled(buffer, "jedit_indent_newline")) {
+        buffer_syntax(buffer) match {
           case Some(syntax) if buffer.isInstanceOf[Buffer] =>
             val keywords = syntax.keywords