proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
authorwenzelm
Sun Jan 24 20:37:40 2016 +0100 (2016-01-24)
changeset 622445d513565749e
parent 62243 dd22d2423047
child 62245 d61174f5cc6d
proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Jan 24 15:30:32 2016 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Jan 24 20:37:40 2016 +0100
     1.3 @@ -166,9 +166,9 @@
     1.4            if (tok.is_command) {
     1.5              if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
     1.6              else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
     1.7 +            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
     1.8              else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
     1.9 -            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3)
    1.10 -            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
    1.11 +            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
    1.12              else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
    1.13              else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
    1.14              else (x, y)