# HG changeset patch
# User wenzelm
# Date 1468317065 -7200
# Node ID 019856db2bb625f6011bd7ec75a55388a94c2349
# Parent  08a1f61a49a6d79273338fd29bc94d823007e915
added action "isabelle.newline" (shortcut ENTER);

diff -r 08a1f61a49a6 -r 019856db2bb6 NEWS
--- a/NEWS	Tue Jul 12 11:12:07 2016 +0200
+++ b/NEWS	Tue Jul 12 11:51:05 2016 +0200
@@ -76,8 +76,12 @@
 
 * Highlighting of entity def/ref positions wrt. cursor.
 
-* Indentation according to Isabelle outer syntax, cf. action
-"indent-lines" (shortcut C+i).
+* Improved support for indentation according to Isabelle outer syntax.
+Action "indent-lines" (shortcut C+i) indents the current line according
+to command keywords and some command substructure. Action
+"isabelle.newline" (shortcut ENTER) indents the old and the new line
+according to command keywords only; see also option
+"jedit_indent_newline".
 
 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
 occurences of the formal entity at the caret position. This facilitates
diff -r 08a1f61a49a6 -r 019856db2bb6 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Jul 12 11:12:07 2016 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Jul 12 11:51:05 2016 +0200
@@ -40,6 +40,12 @@
   -- "default threshold for timing display (seconds)"
 
 
+section "Indentation"
+
+public option jedit_indent_newline : bool = true
+  -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)"
+
+
 section "Completion"
 
 public option jedit_completion : bool = true
diff -r 08a1f61a49a6 -r 019856db2bb6 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Tue Jul 12 11:12:07 2016 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Tue Jul 12 11:51:05 2016 +0200
@@ -62,6 +62,11 @@
 	    isabelle.jedit.Isabelle.decrease_font_size();
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.newline">
+	  <CODE>
+	    isabelle.jedit.Isabelle.newline(textArea);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.select-entity">
 	  <CODE>
 	    isabelle.jedit.Isabelle.select_entity(textArea);
diff -r 08a1f61a49a6 -r 019856db2bb6 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Jul 12 11:12:07 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Jul 12 11:51:05 2016 +0200
@@ -16,7 +16,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher, Selection}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
 import org.gjt.sp.jedit.syntax.TokenMarker
 import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -252,6 +252,51 @@
 
   /* structured edits */
 
+  def newline(text_area: TextArea)
+  {
+    if (!text_area.isEditable()) text_area.getToolkit().beep()
+    else {
+      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 {
+          case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+            val caret = text_area.getCaretPosition
+            val line = text_area.getCaretLine
+            val line_range = JEdit_Lib.line_range(buffer, line)
+
+            def line_content(start: Text.Offset, stop: Text.Offset, context: Scan.Line_Context)
+              : (List[Token], Scan.Line_Context) =
+            {
+              val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
+              val (toks, context1) = Token.explode_line(syntax.keywords, text, context)
+              val toks1 = toks.filterNot(_.is_space)
+              (toks1, context1)
+            }
+
+            val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
+            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_command) buffer.indentLine(line, true)
+
+            if (tokens2.isEmpty || tokens2.head.is_command)
+              JEdit_Lib.buffer_edit(buffer) {
+                text_area.setSelectedText("\n")
+                if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
+              }
+            else nl
+          case _ => nl
+        }
+      }
+      else nl
+    }
+  }
+
   def insert_line_padding(text_area: JEditTextArea, text: String)
   {
     val buffer = text_area.getBuffer
diff -r 08a1f61a49a6 -r 019856db2bb6 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Tue Jul 12 11:12:07 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Jul 12 11:51:05 2016 +0200
@@ -222,6 +222,8 @@
 isabelle.increase-font-size.shortcut=C+PLUS
 isabelle.increase-font-size2.label=Increase font size (clone)
 isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.newline.label=Newline with indentation of Isabelle keywords
+isabelle.newline.shortcut=ENTER
 isabelle.options.label=Isabelle options
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size