include 'begin' and 'end' structure in text folds;
authorwenzelm
Wed Aug 03 11:45:09 2016 +0200 (2016-08-03)
changeset 6359264db21931bcb
parent 63591 8d20875f1290
child 63593 bbcb05504fdc
child 63596 24d329f666c5
child 63603 9d9ea2c6bc38
include 'begin' and 'end' structure in text folds;
NEWS
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/NEWS	Tue Aug 02 22:36:53 2016 +0200
     1.2 +++ b/NEWS	Wed Aug 03 11:45:09 2016 +0200
     1.3 @@ -82,7 +82,8 @@
     1.4  * Highlighting of entity def/ref positions wrt. cursor.
     1.5  
     1.6  * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
     1.7 -are treated as delimiters for fold structure.
     1.8 +are treated as delimiters for fold structure; 'begin' and 'end'
     1.9 +structure of theory specifications is treated as well.
    1.10  
    1.11  * Syntactic indentation according to Isabelle outer syntax. Action
    1.12  "indent-lines" (shortcut C+i) indents the current line according to
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 22:36:53 2016 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Aug 03 11:45:09 2016 +0200
     2.3 @@ -56,7 +56,8 @@
     2.4      command: Boolean = false,
     2.5      depth: Int = 0,
     2.6      span_depth: Int = 0,
     2.7 -    after_span_depth: Int = 0)
     2.8 +    after_span_depth: Int = 0,
     2.9 +    element_depth: Int = 0)
    2.10  
    2.11  
    2.12    /* overall document structure */
    2.13 @@ -157,13 +158,13 @@
    2.14    /* line-oriented structure */
    2.15  
    2.16    private val close_structure =
    2.17 -    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE)
    2.18 +    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
    2.19  
    2.20    def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
    2.21      : Outer_Syntax.Line_Structure =
    2.22    {
    2.23      val improper1 = tokens.forall(_.is_improper)
    2.24 -    val command1 = tokens.exists(_.is_command)
    2.25 +    val command1 = tokens.exists(_.is_begin_or_command)
    2.26  
    2.27      val command_depth =
    2.28        tokens.iterator.filter(_.is_proper).toStream.headOption match {
    2.29 @@ -174,31 +175,36 @@
    2.30          case None => None
    2.31        }
    2.32  
    2.33 +    val depth0 = structure.element_depth
    2.34      val depth1 =
    2.35        if (tokens.exists(tok =>
    2.36 -            keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory))) 0
    2.37 +            keywords.is_before_command(tok) ||
    2.38 +            !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
    2.39        else if (command_depth.isDefined) command_depth.get
    2.40        else if (command1) structure.after_span_depth
    2.41        else structure.span_depth
    2.42  
    2.43 -    val (span_depth1, after_span_depth1) =
    2.44 -      ((structure.span_depth, structure.after_span_depth) /: tokens) {
    2.45 -        case ((x, y), tok) =>
    2.46 -          if (tok.is_command) {
    2.47 -            if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
    2.48 -            else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
    2.49 -            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
    2.50 -            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
    2.51 -            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
    2.52 -            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
    2.53 -            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    2.54 -            else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    2.55 -            else (x, y)
    2.56 +    val (span_depth1, after_span_depth1, element_depth1) =
    2.57 +      ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
    2.58 +        case (depths @ (x, y, z), tok) =>
    2.59 +          if (tok.is_begin) (z + 2, z + 1, z + 1)
    2.60 +          else if (tok.is_end) (z + 1, z - 1, z - 1)
    2.61 +          else if (tok.is_command) {
    2.62 +            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
    2.63 +            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
    2.64 +            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
    2.65 +            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
    2.66 +            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
    2.67 +            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
    2.68 +            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
    2.69 +            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
    2.70 +            else depths
    2.71            }
    2.72 -          else (x, y)
    2.73 +          else depths
    2.74        }
    2.75  
    2.76 -    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
    2.77 +    Outer_Syntax.Line_Structure(
    2.78 +      improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    2.79    }
    2.80  
    2.81