--- 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
--- 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
--- 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);
--- 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
--- 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