Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
authorwenzelm
Sun, 24 Jan 2016 20:37:40 +0100
changeset 62244 5d513565749e
parent 62243 dd22d2423047
child 62245 d61174f5cc6d
proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
src/Pure/Isar/outer_syntax.scala file | annotate | diff | comparison | revisions 
--- 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)
isabelle