semantic indentation for unstructured proof scripts;
authorwenzelm
Wed Jul 13 15:19:16 2016 +0200 (2016-07-13 ago)
changeset 63474f66e3c3b0fb1
parent 63473 151bb79536a7
child 63475 31016a88197b
semantic indentation for unstructured proof scripts;
NEWS
src/Pure/PIDE/command.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/NEWS	Wed Jul 13 14:28:15 2016 +0200
     1.2 +++ b/NEWS	Wed Jul 13 15:19:16 2016 +0200
     1.3 @@ -79,13 +79,19 @@
     1.4  * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
     1.5  are treated as delimiters for fold structure.
     1.6  
     1.7 -* Improved support for indentation according to Isabelle outer syntax.
     1.8 -Action "indent-lines" (shortcut C+i) indents the current line according
     1.9 -to command keywords and some command substructure. Action
    1.10 +* Syntactic indentation according to Isabelle outer syntax. Action
    1.11 +"indent-lines" (shortcut C+i) indents the current line according to
    1.12 +command keywords and some command substructure. Action
    1.13  "isabelle.newline" (shortcut ENTER) indents the old and the new line
    1.14  according to command keywords only; see also option
    1.15  "jedit_indent_newline".
    1.16  
    1.17 +* Semantic indentation for unstructured proof scripts ('apply' etc.) via
    1.18 +number of subgoals. This requires information of ongoing document
    1.19 +processing and may thus lag behind, when the user is editing too
    1.20 +quickly; see also option "jedit_script_indent" and
    1.21 +"jedit_script_indent_limit".
    1.22 +
    1.23  * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
    1.24  occurences of the formal entity at the caret position. This facilitates
    1.25  systematic renaming.
     2.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 13 14:28:15 2016 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 13 15:19:16 2016 +0200
     2.3 @@ -214,12 +214,28 @@
     2.4      SOME prf => status tr (Proof.status_markup prf)
     2.5    | NONE => ());
     2.6  
     2.7 +fun command_indent tr st =
     2.8 +  (case try Toplevel.proof_of st of
     2.9 +    SOME prf =>
    2.10 +      let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in
    2.11 +        if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then
    2.12 +          (case try Proof.goal prf of
    2.13 +            SOME {goal, ...} =>
    2.14 +              let val n = Thm.nprems_of goal
    2.15 +              in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end
    2.16 +          | NONE => ())
    2.17 +        else ()
    2.18 +      end
    2.19 +  | NONE => ());
    2.20 +
    2.21 +
    2.22  fun eval_state keywords span tr ({state, ...}: eval_state) =
    2.23    let
    2.24      val _ = Thread_Attributes.expose_interrupt ();
    2.25  
    2.26      val st = reset_state keywords tr state;
    2.27  
    2.28 +    val _ = command_indent tr st;
    2.29      val _ = status tr Markup.running;
    2.30      val (errs1, result) = run keywords true tr st;
    2.31      val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
     3.1 --- a/src/Pure/PIDE/markup.ML	Wed Jul 13 14:28:15 2016 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jul 13 15:19:16 2016 +0200
     3.3 @@ -155,6 +155,7 @@
     3.4    val parse_command_timing_properties:
     3.5      Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
     3.6    val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
     3.7 +  val command_indentN: string val command_indent: int -> T
     3.8    val subgoalsN: string
     3.9    val proof_stateN: string val proof_state: int -> T
    3.10    val goalN: string val goal: T
    3.11 @@ -576,7 +577,12 @@
    3.12    | _ => NONE);
    3.13  
    3.14  
    3.15 -(* toplevel *)
    3.16 +(* indentation *)
    3.17 +
    3.18 +val (command_indentN, command_indent) = markup_int "command_indent" indentN;
    3.19 +
    3.20 +
    3.21 +(* goals *)
    3.22  
    3.23  val subgoalsN = "subgoals";
    3.24  val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
     4.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 13 14:28:15 2016 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 13 15:19:16 2016 +0200
     4.3 @@ -372,7 +372,17 @@
     4.4    val COMMAND_TIMING = "command_timing"
     4.5  
     4.6  
     4.7 -  /* toplevel */
     4.8 +  /* command indentation */
     4.9 +
    4.10 +  object Command_Indent
    4.11 +  {
    4.12 +    val name = "command_indent"
    4.13 +    def unapply(markup: Markup): Option[Int] =
    4.14 +      if (markup.name == name) Indent.unapply(markup.properties) else None
    4.15 +  }
    4.16 +
    4.17 +
    4.18 +  /* goals */
    4.19  
    4.20    val SUBGOALS = "subgoals"
    4.21    val PROOF_STATE = "proof_state"
     5.1 --- a/src/Tools/jEdit/etc/options	Wed Jul 13 14:28:15 2016 +0200
     5.2 +++ b/src/Tools/jEdit/etc/options	Wed Jul 13 15:19:16 2016 +0200
     5.3 @@ -45,6 +45,12 @@
     5.4  public option jedit_indent_newline : bool = true
     5.5    -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)"
     5.6  
     5.7 +public option jedit_indent_script : bool = true
     5.8 +  -- "indent unstructured proof script ('apply' etc.) via number of subgoals"
     5.9 +
    5.10 +public option jedit_indent_script_limit : int = 20
    5.11 +  -- "maximum indentation of unstructured proof script ('apply' etc.)"
    5.12 +
    5.13  
    5.14  section "Completion"
    5.15  
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Jul 13 14:28:15 2016 +0200
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Jul 13 15:19:16 2016 +0200
     6.3 @@ -137,6 +137,9 @@
     6.4  
     6.5    /* markup elements */
     6.6  
     6.7 +  private val indentation_elements =
     6.8 +    Markup.Elements(Markup.Command_Indent.name)
     6.9 +
    6.10    private val semantic_completion_elements =
    6.11      Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    6.12  
    6.13 @@ -295,6 +298,16 @@
    6.14    val markdown_item_color4 = color_value("markdown_item_color4")
    6.15  
    6.16  
    6.17 +  /* indentation */
    6.18 +
    6.19 +  def indentation(range: Text.Range): Int =
    6.20 +    snapshot.select(range, Rendering.indentation_elements, _ =>
    6.21 +      {
    6.22 +        case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
    6.23 +        case _ => None
    6.24 +      }).headOption.map(_.info).getOrElse(0)
    6.25 +
    6.26 +
    6.27    /* completion */
    6.28  
    6.29    def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
     7.1 --- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 14:28:15 2016 +0200
     7.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 15:19:16 2016 +0200
     7.3 @@ -52,13 +52,20 @@
     7.4            val keywords = syntax.keywords
     7.5            val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
     7.6  
     7.7 -          def head_token(line: Int): Option[Token] =
     7.8 -            nav.iterator(line, 1).toStream.headOption.map(_.info)
     7.9 +          val indent_size = buffer.getIndentSize
    7.10 +
    7.11 +
    7.12 +          def line_indent(line: Int): Int =
    7.13 +            if (line < 0 || line >= buffer.getLineCount) 0
    7.14 +            else buffer.getCurrentIndentForLine(line, null)
    7.15 +
    7.16 +          def line_head(line: Int): Option[Text.Info[Token]] =
    7.17 +            nav.iterator(line, 1).toStream.headOption
    7.18  
    7.19            def head_is_quasi_command(line: Int): Boolean =
    7.20 -            head_token(line) match {
    7.21 +            line_head(line) match {
    7.22                case None => false
    7.23 -              case Some(tok) => keywords.is_quasi_command(tok)
    7.24 +              case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
    7.25              }
    7.26  
    7.27            def prev_command: Option[Token] =
    7.28 @@ -72,11 +79,24 @@
    7.29              nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command)
    7.30  
    7.31  
    7.32 -          def line_indent(line: Int): Int =
    7.33 -            if (line < 0 || line >= buffer.getLineCount) 0
    7.34 -            else buffer.getCurrentIndentForLine(line, null)
    7.35 -
    7.36 -          val indent_size = buffer.getIndentSize
    7.37 +          val script_indent: Text.Range => Int =
    7.38 +          {
    7.39 +            val opt_rendering: Option[Rendering] =
    7.40 +              if (PIDE.options.value.bool("jedit_indent_script"))
    7.41 +                GUI_Thread.now {
    7.42 +                  (for {
    7.43 +                    text_area <- JEdit_Lib.jedit_text_areas(buffer)
    7.44 +                    doc_view <- PIDE.document_view(text_area)
    7.45 +                  } yield doc_view.get_rendering).toStream.headOption
    7.46 +                }
    7.47 +              else None
    7.48 +            val limit = PIDE.options.value.int("jedit_indent_script_limit")
    7.49 +            (range: Text.Range) =>
    7.50 +              opt_rendering match {
    7.51 +                case Some(rendering) => (rendering.indentation(range) min limit) max 0
    7.52 +                case None => 0
    7.53 +              }
    7.54 +          }
    7.55  
    7.56            def indent_indent(tok: Token): Int =
    7.57              if (keywords.is_command(tok, keyword_open)) indent_size
    7.58 @@ -102,11 +122,13 @@
    7.59              nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
    7.60                { case ((ind, _), Text.Info(range, tok)) =>
    7.61                    val ind1 = ind + indent_indent(tok)
    7.62 -                  if (tok.is_command) {
    7.63 +                  if (tok.is_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
    7.64                      val line = buffer.getLineOfOffset(range.start)
    7.65 -                    if (head_token(line) == Some(tok))
    7.66 -                      (ind1 + indent_offset(tok) + line_indent(line), true)
    7.67 -                    else (ind1, false)
    7.68 +                    line_head(line) match {
    7.69 +                      case Some(info) if info.info == tok =>
    7.70 +                        (ind1 + indent_offset(tok) + line_indent(line), true)
    7.71 +                      case _ => (ind1, false)
    7.72 +                    }
    7.73                    }
    7.74                    else (ind1, false)
    7.75                }).collectFirst({ case (i, true) => i }).getOrElse(0)
    7.76 @@ -119,12 +141,15 @@
    7.77                indent_size
    7.78  
    7.79            val indent =
    7.80 -            head_token(current_line) match {
    7.81 +            line_head(current_line) match {
    7.82                case None => indent_structure + indent_brackets + indent_extra
    7.83 -              case Some(tok) =>
    7.84 +              case Some(Text.Info(range, tok)) =>
    7.85                  if (keywords.is_before_command(tok) ||
    7.86                      keywords.is_command(tok, Keyword.theory)) indent_begin
    7.87 -                else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
    7.88 +                else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
    7.89 +                  indent_structure + script_indent(range)
    7.90 +                else if (tok.is_command)
    7.91 +                  indent_structure + indent_begin - indent_offset(tok)
    7.92                  else {
    7.93                    prev_command match {
    7.94                      case None =>