--- a/NEWS Wed Jul 13 14:28:15 2016 +0200
+++ b/NEWS Wed Jul 13 15:19:16 2016 +0200
@@ -79,13 +79,19 @@
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure.
-* 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
+* Syntactic 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".
+* Semantic indentation for unstructured proof scripts ('apply' etc.) via
+number of subgoals. This requires information of ongoing document
+processing and may thus lag behind, when the user is editing too
+quickly; see also option "jedit_script_indent" and
+"jedit_script_indent_limit".
+
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurences of the formal entity at the caret position. This facilitates
systematic renaming.
--- a/src/Pure/PIDE/command.ML Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Pure/PIDE/command.ML Wed Jul 13 15:19:16 2016 +0200
@@ -214,12 +214,28 @@
SOME prf => status tr (Proof.status_markup prf)
| NONE => ());
+fun command_indent tr st =
+ (case try Toplevel.proof_of st of
+ SOME prf =>
+ let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in
+ if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then
+ (case try Proof.goal prf of
+ SOME {goal, ...} =>
+ let val n = Thm.nprems_of goal
+ in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end
+ | NONE => ())
+ else ()
+ end
+ | NONE => ());
+
+
fun eval_state keywords span tr ({state, ...}: eval_state) =
let
val _ = Thread_Attributes.expose_interrupt ();
val st = reset_state keywords tr state;
+ val _ = command_indent tr st;
val _ = status tr Markup.running;
val (errs1, result) = run keywords true tr st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
--- a/src/Pure/PIDE/markup.ML Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Jul 13 15:19:16 2016 +0200
@@ -155,6 +155,7 @@
val parse_command_timing_properties:
Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
+ val command_indentN: string val command_indent: int -> T
val subgoalsN: string
val proof_stateN: string val proof_state: int -> T
val goalN: string val goal: T
@@ -576,7 +577,12 @@
| _ => NONE);
-(* toplevel *)
+(* indentation *)
+
+val (command_indentN, command_indent) = markup_int "command_indent" indentN;
+
+
+(* goals *)
val subgoalsN = "subgoals";
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
--- a/src/Pure/PIDE/markup.scala Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Jul 13 15:19:16 2016 +0200
@@ -372,7 +372,17 @@
val COMMAND_TIMING = "command_timing"
- /* toplevel */
+ /* command indentation */
+
+ object Command_Indent
+ {
+ val name = "command_indent"
+ def unapply(markup: Markup): Option[Int] =
+ if (markup.name == name) Indent.unapply(markup.properties) else None
+ }
+
+
+ /* goals */
val SUBGOALS = "subgoals"
val PROOF_STATE = "proof_state"
--- a/src/Tools/jEdit/etc/options Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Tools/jEdit/etc/options Wed Jul 13 15:19:16 2016 +0200
@@ -45,6 +45,12 @@
public option jedit_indent_newline : bool = true
-- "indentation of Isabelle keywords on ENTER (action isabelle.newline)"
+public option jedit_indent_script : bool = true
+ -- "indent unstructured proof script ('apply' etc.) via number of subgoals"
+
+public option jedit_indent_script_limit : int = 20
+ -- "maximum indentation of unstructured proof script ('apply' etc.)"
+
section "Completion"
--- a/src/Tools/jEdit/src/rendering.scala Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Jul 13 15:19:16 2016 +0200
@@ -137,6 +137,9 @@
/* markup elements */
+ private val indentation_elements =
+ Markup.Elements(Markup.Command_Indent.name)
+
private val semantic_completion_elements =
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
@@ -295,6 +298,16 @@
val markdown_item_color4 = color_value("markdown_item_color4")
+ /* indentation */
+
+ def indentation(range: Text.Range): Int =
+ snapshot.select(range, Rendering.indentation_elements, _ =>
+ {
+ case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
+ case _ => None
+ }).headOption.map(_.info).getOrElse(0)
+
+
/* completion */
def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
--- a/src/Tools/jEdit/src/text_structure.scala Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Wed Jul 13 15:19:16 2016 +0200
@@ -52,13 +52,20 @@
val keywords = syntax.keywords
val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
- def head_token(line: Int): Option[Token] =
- nav.iterator(line, 1).toStream.headOption.map(_.info)
+ val indent_size = buffer.getIndentSize
+
+
+ def line_indent(line: Int): Int =
+ if (line < 0 || line >= buffer.getLineCount) 0
+ else buffer.getCurrentIndentForLine(line, null)
+
+ def line_head(line: Int): Option[Text.Info[Token]] =
+ nav.iterator(line, 1).toStream.headOption
def head_is_quasi_command(line: Int): Boolean =
- head_token(line) match {
+ line_head(line) match {
case None => false
- case Some(tok) => keywords.is_quasi_command(tok)
+ case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
}
def prev_command: Option[Token] =
@@ -72,11 +79,24 @@
nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command)
- def line_indent(line: Int): Int =
- if (line < 0 || line >= buffer.getLineCount) 0
- else buffer.getCurrentIndentForLine(line, null)
-
- val indent_size = buffer.getIndentSize
+ val script_indent: Text.Range => Int =
+ {
+ val opt_rendering: Option[Rendering] =
+ if (PIDE.options.value.bool("jedit_indent_script"))
+ GUI_Thread.now {
+ (for {
+ text_area <- JEdit_Lib.jedit_text_areas(buffer)
+ doc_view <- PIDE.document_view(text_area)
+ } yield doc_view.get_rendering).toStream.headOption
+ }
+ else None
+ val limit = PIDE.options.value.int("jedit_indent_script_limit")
+ (range: Text.Range) =>
+ opt_rendering match {
+ case Some(rendering) => (rendering.indentation(range) min limit) max 0
+ case None => 0
+ }
+ }
def indent_indent(tok: Token): Int =
if (keywords.is_command(tok, keyword_open)) indent_size
@@ -102,11 +122,13 @@
nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
{ case ((ind, _), Text.Info(range, tok)) =>
val ind1 = ind + indent_indent(tok)
- if (tok.is_command) {
+ if (tok.is_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
val line = buffer.getLineOfOffset(range.start)
- if (head_token(line) == Some(tok))
- (ind1 + indent_offset(tok) + line_indent(line), true)
- else (ind1, false)
+ line_head(line) match {
+ case Some(info) if info.info == tok =>
+ (ind1 + indent_offset(tok) + line_indent(line), true)
+ case _ => (ind1, false)
+ }
}
else (ind1, false)
}).collectFirst({ case (i, true) => i }).getOrElse(0)
@@ -119,12 +141,15 @@
indent_size
val indent =
- head_token(current_line) match {
+ line_head(current_line) match {
case None => indent_structure + indent_brackets + indent_extra
- case Some(tok) =>
+ case Some(Text.Info(range, tok)) =>
if (keywords.is_before_command(tok) ||
keywords.is_command(tok, Keyword.theory)) indent_begin
- else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
+ else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
+ indent_structure + script_indent(range)
+ else if (tok.is_command)
+ indent_structure + indent_begin - indent_offset(tok)
else {
prev_command match {
case None =>