# HG changeset patch
# User wenzelm
# Date 1436350184 -7200
# Node ID 896704918a1fdac73529a989f2fbed4d9404f474
# Parent  0568c7a2b5dbb343d819bf64ab9879e20c210bda
tuned;

diff -r 0568c7a2b5db -r 896704918a1f src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Jul 08 11:50:43 2015 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Jul 08 12:09:44 2015 +0200
@@ -77,6 +77,9 @@
   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   val qed_global = Set(QED_GLOBAL)
 
+  val proof_open = proof_goal + PRF_OPEN
+  val proof_close = qed + PRF_CLOSE
+
 
 
   /** keyword tables **/
diff -r 0568c7a2b5db -r 896704918a1f src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 11:50:43 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 12:09:44 2015 +0200
@@ -164,16 +164,11 @@
       ((structure.span_depth, structure.after_span_depth) /: tokens) {
         case ((x, y), tok) =>
           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_goal) || tok.is_begin_block)
-              (y + 2, y + 1)
-            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
-              (y + 1, y - 1)
-            else if (tok.is_command_kind(keywords, Keyword.qed_global))
-              (1, 0)
+            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.proof_close)) (y + 1, y - 1)
+            else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
             else (x, y)
           }
           else (x, y)
diff -r 0568c7a2b5db -r 896704918a1f src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Jul 08 11:50:43 2015 +0200
+++ b/src/Pure/Isar/token.scala	Wed Jul 08 12:09:44 2015 +0200
@@ -263,9 +263,6 @@
   def is_command_modifier: Boolean =
     is_keyword && (source == "public" || source == "private" || source == "qualified")
 
-  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)