# HG changeset patch # User wenzelm # Date 1498249550 -7200 # Node ID 8328467d32f4d3a8ee2078d4fd3df745a4b292ca # Parent df70049d584dc6ddbf9c04d8626e7d2ea3987e68# Parent c67933ea9234691fc6350bbf843863bdcf75757a merged diff -r df70049d584d -r 8328467d32f4 NEWS --- 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. diff -r df70049d584d -r 8328467d32f4 src/Pure/Isar/line_structure.scala --- 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) } } diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/etc/options --- 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)" diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/src/completion_popup.scala --- 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) } } diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/src/fold_handling.scala --- 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 diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/src/isabelle.scala --- 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 diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/src/text_structure.scala --- 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 } } diff -r df70049d584d -r 8328467d32f4 src/Tools/jEdit/src/token_markup.scala --- 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))