tuned;
authorwenzelm
Tue Oct 21 20:44:17 2014 +0200 (2014-10-21)
changeset 58753960bf499ca5d
parent 58752 2077bc9558cf
child 58754 0232d43422d6
tuned;
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 20:19:14 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 20:44:17 2014 +0200
     1.3 @@ -192,8 +192,8 @@
     1.4            if (tok.is_command) {
     1.5              if (command_kind(tok, Keyword.theory_goal)) (2, 1)
     1.6              else if (command_kind(tok, Keyword.theory)) (1, 0)
     1.7 -            else if (command_kind(tok, Keyword.proof_goal) || tok.source == "{") (y + 2, y + 1)
     1.8 -            else if (command_kind(tok, Keyword.qed) || tok.source == "}") (y + 1, y - 1)
     1.9 +            else if (command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) (y + 2, y + 1)
    1.10 +            else if (command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1)
    1.11              else if (command_kind(tok, Keyword.qed_global)) (1, 0)
    1.12              else (x, y)
    1.13            }
     2.1 --- a/src/Pure/Isar/token.scala	Tue Oct 21 20:19:14 2014 +0200
     2.2 +++ b/src/Pure/Isar/token.scala	Tue Oct 21 20:44:17 2014 +0200
     2.3 @@ -192,6 +192,9 @@
     2.4    def is_begin: Boolean = is_keyword && source == "begin"
     2.5    def is_end: Boolean = is_command && source == "end"
     2.6  
     2.7 +  def is_begin_block: Boolean = is_command && source == "{"
     2.8 +  def is_end_block: Boolean = is_command && source == "}"
     2.9 +
    2.10    def content: String =
    2.11      if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
    2.12      else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)