--- a/NEWS Fri Jun 23 15:01:06 2017 +0200
+++ b/NEWS Fri Jun 23 22:25:50 2017 +0200
@@ -52,6 +52,10 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Automatic indentation is more careful to avoid redundant spaces in
+intermediate situations. Keywords are indented after input (via typed
+characters or completion); see also option "jedit_indent_input".
+
* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.
--- a/src/Pure/Isar/line_structure.scala Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Pure/Isar/line_structure.scala Fri Jun 23 22:25:50 2017 +0200
@@ -14,6 +14,7 @@
sealed case class Line_Structure(
improper: Boolean = true,
+ blank: Boolean = true,
command: Boolean = false,
depth: Int = 0,
span_depth: Int = 0,
@@ -23,6 +24,7 @@
def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
{
val improper1 = tokens.forall(_.is_improper)
+ val blank1 = tokens.forall(_.is_space)
val command1 = tokens.exists(_.is_begin_or_command)
val command_depth =
@@ -62,6 +64,7 @@
else depths
}
- Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
+ Line_Structure(
+ improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
}
}
--- a/src/Tools/jEdit/etc/options Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/etc/options Fri Jun 23 22:25:50 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 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Jun 23 22:25:50 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/fold_handling.scala Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Fri Jun 23 22:25:50 2017 +0200
@@ -29,16 +29,16 @@
}
override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
- Token_Markup.Line_Context.next(buffer, line).structure.depth max 0
+ Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
override def getPrecedingFoldLevels(
buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
{
- val structure = Token_Markup.Line_Context.next(buffer, line).structure
+ val structure = Token_Markup.Line_Context.after(buffer, line).structure
val result =
if (line > 0 && structure.command)
Range.inclusive(line - 1, 0, -1).iterator.
- map(i => Token_Markup.Line_Context.next(buffer, i).structure).
+ map(i => Token_Markup.Line_Context.after(buffer, i).structure).
takeWhile(_.improper).map(_ => structure.depth max 0).toList
else Nil
--- a/src/Tools/jEdit/src/isabelle.scala Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Jun 23 22:25:50 2017 +0200
@@ -244,48 +244,59 @@
/* 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) =>
+ val nav = new Text_Structure.Navigator(syntax, 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 None =>
+ }
+ }
+ }
+
def newline(text_area: TextArea)
{
if (!text_area.isEditable()) text_area.getToolkit().beep()
else {
val buffer = text_area.getBuffer
+ val line = text_area.getCaretLine
+ val caret = text_area.getCaretPosition
+
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] =>
+ if (indent_enabled(buffer, "jedit_indent_newline")) {
+ buffer_syntax(buffer) match {
+ case Some(syntax) =>
val keywords = syntax.keywords
- val caret = text_area.getCaretPosition
- val line = text_area.getCaretLine
- val line_range = JEdit_Lib.line_range(buffer, line)
+ val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
- 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(keywords, text, context)
- val toks1 = toks.filterNot(_.is_space)
- (toks1, context1)
- }
+ if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
+ else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)
- 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 && keywords.is_indent_command(tokens1.head))
- buffer.indentLine(line, true)
-
- if (tokens2.isEmpty || keywords.is_indent_command(tokens2.head))
+ if (toks2.isEmpty || keywords.is_indent_command(toks2.head))
JEdit_Lib.buffer_edit(buffer) {
text_area.setSelectedText("\n")
if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
}
else nl
- case _ => nl
+ case None => nl
}
}
else nl
--- a/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 22:25:50 2017 +0200
@@ -19,7 +19,7 @@
{
/* token navigator */
- class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
+ class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean)
{
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
@@ -48,9 +48,9 @@
actions: java.util.List[IndentAction])
{
Isabelle.buffer_syntax(buffer) match {
- case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+ case Some(syntax) =>
val keywords = syntax.keywords
- val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
+ val nav = new Navigator(syntax, buffer, true)
val indent_size = buffer.getIndentSize
@@ -70,8 +70,9 @@
val prev_line: Int =
Range.inclusive(current_line - 1, 0, -1).find(line =>
- Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
- !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
+ Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished &&
+ (!Token_Markup.Line_Context.after(buffer, line).structure.improper ||
+ Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1
def prev_line_command: Option[Token] =
nav.reverse_iterator(prev_line, 1).
@@ -140,7 +141,10 @@
else 0
val indent =
- if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
+ if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished)
+ line_indent(current_line)
+ else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
+ else {
line_head(current_line) match {
case Some(info @ Text.Info(range, tok)) =>
if (tok.is_begin ||
@@ -177,15 +181,33 @@
}
}
}
- else line_indent(current_line)
actions.clear()
actions.add(new IndentAction.AlignOffset(indent max 0))
- case _ =>
+ case None =>
}
}
}
+ def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
+ range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) =
+ {
+ val text = JEdit_Lib.try_get_text(buffer, range).getOrElse("")
+ val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt)
+ val toks1 = toks.filterNot(_.is_space)
+ (toks1, ctxt1)
+ }
+
+ def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int)
+ : (List[Token], List[Token]) =
+ {
+ val line_range = JEdit_Lib.line_range(buffer, line)
+ val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context
+ val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0)
+ val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1)
+ (toks1, toks2)
+ }
+
/* structure matching */
@@ -216,10 +238,10 @@
val caret = text_area.getCaretPosition
Isabelle.buffer_syntax(text_area.getBuffer) match {
- case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+ case Some(syntax) =>
val keywords = syntax.keywords
- val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
+ val nav = new Navigator(syntax, buffer, false)
def caret_iterator(): Iterator[Text.Info[Token]] =
nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
@@ -292,7 +314,7 @@
case _ => None
}
- case _ => None
+ case None => None
}
}
--- a/src/Tools/jEdit/src/token_markup.scala Fri Jun 23 15:01:06 2017 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Fri Jun 23 22:25:50 2017 +0200
@@ -29,11 +29,11 @@
def init(mode: String): Line_Context =
new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
- def prev(buffer: JEditBuffer, line: Int): Line_Context =
+ def before(buffer: JEditBuffer, line: Int): Line_Context =
if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
- else next(buffer, line - 1)
+ else after(buffer, line - 1)
- def next(buffer: JEditBuffer, line: Int): Line_Context =
+ def after(buffer: JEditBuffer, line: Int): Line_Context =
{
val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
def context =
@@ -71,7 +71,7 @@
private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
: Option[List[Token]] =
{
- val line_context = Line_Context.prev(buffer, line)
+ val line_context = Line_Context.before(buffer, line)
for {
ctxt <- line_context.context
text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))