src/Pure/Isar/outer_syntax.scala
changeset 63592 64db21931bcb
parent 63587 881e8e2cfec2
child 63603 9d9ea2c6bc38
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 22:36:53 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Aug 03 11:45:09 2016 +0200
     1.3 @@ -56,7 +56,8 @@
     1.4      command: Boolean = false,
     1.5      depth: Int = 0,
     1.6      span_depth: Int = 0,
     1.7 -    after_span_depth: Int = 0)
     1.8 +    after_span_depth: Int = 0,
     1.9 +    element_depth: Int = 0)
    1.10  
    1.11  
    1.12    /* overall document structure */
    1.13 @@ -157,13 +158,13 @@
    1.14    /* line-oriented structure */
    1.15  
    1.16    private val close_structure =
    1.17 -    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE)
    1.18 +    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
    1.19  
    1.20    def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
    1.21      : Outer_Syntax.Line_Structure =
    1.22    {
    1.23      val improper1 = tokens.forall(_.is_improper)
    1.24 -    val command1 = tokens.exists(_.is_command)
    1.25 +    val command1 = tokens.exists(_.is_begin_or_command)
    1.26  
    1.27      val command_depth =
    1.28        tokens.iterator.filter(_.is_proper).toStream.headOption match {
    1.29 @@ -174,31 +175,36 @@
    1.30          case None => None
    1.31        }
    1.32  
    1.33 +    val depth0 = structure.element_depth
    1.34      val depth1 =
    1.35        if (tokens.exists(tok =>
    1.36 -            keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory))) 0
    1.37 +            keywords.is_before_command(tok) ||
    1.38 +            !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
    1.39        else if (command_depth.isDefined) command_depth.get
    1.40        else if (command1) structure.after_span_depth
    1.41        else structure.span_depth
    1.42  
    1.43 -    val (span_depth1, after_span_depth1) =
    1.44 -      ((structure.span_depth, structure.after_span_depth) /: tokens) {
    1.45 -        case ((x, y), tok) =>
    1.46 -          if (tok.is_command) {
    1.47 -            if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
    1.48 -            else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
    1.49 -            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
    1.50 -            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
    1.51 -            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
    1.52 -            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
    1.53 -            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    1.54 -            else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    1.55 -            else (x, y)
    1.56 +    val (span_depth1, after_span_depth1, element_depth1) =
    1.57 +      ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
    1.58 +        case (depths @ (x, y, z), tok) =>
    1.59 +          if (tok.is_begin) (z + 2, z + 1, z + 1)
    1.60 +          else if (tok.is_end) (z + 1, z - 1, z - 1)
    1.61 +          else if (tok.is_command) {
    1.62 +            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
    1.63 +            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
    1.64 +            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
    1.65 +            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
    1.66 +            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
    1.67 +            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
    1.68 +            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
    1.69 +            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
    1.70 +            else depths
    1.71            }
    1.72 -          else (x, y)
    1.73 +          else depths
    1.74        }
    1.75  
    1.76 -    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
    1.77 +    Outer_Syntax.Line_Structure(
    1.78 +      improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    1.79    }
    1.80  
    1.81