src/Pure/Isar/outer_syntax.scala
changeset 60692 896704918a1f
parent 60215 5fb4990dfc73
child 60694 b3fa4a8cdb5f
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 11:50:43 2015 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 12:09:44 2015 +0200
     1.3 @@ -164,16 +164,11 @@
     1.4        ((structure.span_depth, structure.after_span_depth) /: tokens) {
     1.5          case ((x, y), tok) =>
     1.6            if (tok.is_command) {
     1.7 -            if (tok.is_command_kind(keywords, Keyword.theory_goal))
     1.8 -              (2, 1)
     1.9 -            else if (tok.is_command_kind(keywords, Keyword.theory))
    1.10 -              (1, 0)
    1.11 -            else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
    1.12 -              (y + 2, y + 1)
    1.13 -            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
    1.14 -              (y + 1, y - 1)
    1.15 -            else if (tok.is_command_kind(keywords, Keyword.qed_global))
    1.16 -              (1, 0)
    1.17 +            if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
    1.18 +            else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
    1.19 +            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
    1.20 +            else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
    1.21 +            else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
    1.22              else (x, y)
    1.23            }
    1.24            else (x, y)