# HG changeset patch
# User wenzelm
# Date 1453664260 -3600
# Node ID 5d513565749e6818ce3bbd1b40739ddc314e17a5
# Parent  dd22d242304792f10dc2733ece6a811df39f68fa
proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;

diff -r dd22d2423047 -r 5d513565749e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sun Jan 24 15:30:32 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sun Jan 24 20:37:40 2016 +0100
@@ -166,9 +166,9 @@
           if (tok.is_command) {
             if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
             else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
+            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
             else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
-            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3)
-            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
+            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
             else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
             else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
             else (x, y)