--- 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)