closing 'qed' or '}' is outside of fold;
authorwenzelm
Tue Jul 12 13:26:39 2016 +0200 (2016-07-12)
changeset 63458723f9c673c1c
parent 63457 be6ceddff102
child 63459 8d68204d97d7
closing 'qed' or '}' is outside of fold;
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 12:58:53 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 13:26:39 2016 +0200
     1.3 @@ -148,8 +148,20 @@
     1.4      val improper1 = tokens.forall(_.is_improper)
     1.5      val command1 = tokens.exists(_.is_command)
     1.6  
     1.7 +    val command_depth =
     1.8 +      tokens.iterator.filter(_.is_proper).toStream.headOption match {
     1.9 +        case Some(tok) =>
    1.10 +          if (keywords.is_command(tok, Keyword.QED_BLOCK == _))
    1.11 +            Some(structure.after_span_depth - 2)
    1.12 +          else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _))
    1.13 +            Some(structure.after_span_depth - 1)
    1.14 +          else None
    1.15 +        case None => None
    1.16 +      }
    1.17 +
    1.18      val depth1 =
    1.19        if (tokens.exists(keywords.is_command(_, Keyword.theory))) 0
    1.20 +      else if (command_depth.isDefined) command_depth.get
    1.21        else if (command1) structure.after_span_depth
    1.22        else structure.span_depth
    1.23  
    1.24 @@ -161,7 +173,8 @@
    1.25              else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
    1.26              else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
    1.27              else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
    1.28 -            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
    1.29 +            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
    1.30 +            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
    1.31              else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    1.32              else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    1.33              else (x, y)