# HG changeset patch
# User wenzelm
# Date 1468415956 -7200
# Node ID f66e3c3b0fb1f6eacf6b72639dd8bb5516753ed4
# Parent  151bb79536a75eafe5c00dbb6c5246b03a888cd6
semantic indentation for unstructured proof scripts;

diff -r 151bb79536a7 -r f66e3c3b0fb1 NEWS
--- 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.
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Pure/PIDE/command.ML
--- 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');
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Pure/PIDE/markup.ML
--- 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;
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Pure/PIDE/markup.scala
--- 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"
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Tools/jEdit/etc/options
--- 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"
 
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Tools/jEdit/src/rendering.scala
--- 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)
diff -r 151bb79536a7 -r f66e3c3b0fb1 src/Tools/jEdit/src/text_structure.scala
--- 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 =>