# HG changeset patch
# User wenzelm
# Date 1413917057 -7200
# Node ID 960bf499ca5de1d27a91bf7914454681f7446aa9
# Parent  2077bc9558cfefc2eb3df206f97d071386bd2629
tuned;

diff -r 2077bc9558cf -r 960bf499ca5d src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 20:19:14 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 20:44:17 2014 +0200
@@ -192,8 +192,8 @@
           if (tok.is_command) {
             if (command_kind(tok, Keyword.theory_goal)) (2, 1)
             else if (command_kind(tok, Keyword.theory)) (1, 0)
-            else if (command_kind(tok, Keyword.proof_goal) || tok.source == "{") (y + 2, y + 1)
-            else if (command_kind(tok, Keyword.qed) || tok.source == "}") (y + 1, y - 1)
+            else if (command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) (y + 2, y + 1)
+            else if (command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1)
             else if (command_kind(tok, Keyword.qed_global)) (1, 0)
             else (x, y)
           }
diff -r 2077bc9558cf -r 960bf499ca5d src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Oct 21 20:19:14 2014 +0200
+++ b/src/Pure/Isar/token.scala	Tue Oct 21 20:44:17 2014 +0200
@@ -192,6 +192,9 @@
   def is_begin: Boolean = is_keyword && source == "begin"
   def is_end: Boolean = is_command && source == "end"
 
+  def is_begin_block: Boolean = is_command && source == "{"
+  def is_end_block: Boolean = is_command && source == "}"
+
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
     else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)