src/Pure/Isar/outer_syntax.scala
changeset 63424 e4e15bbfb3e2
parent 62453 b93cc7d73431
child 63429 baedd4724f08
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Jul 07 21:10:12 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Jul 07 21:34:56 2016 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4      val command1 = tokens.exists(_.is_command)
     1.5  
     1.6      val depth1 =
     1.7 -      if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
     1.8 +      if (tokens.exists(keywords.is_command(_, Keyword.theory))) 0
     1.9        else if (command1) structure.after_span_depth
    1.10        else structure.span_depth
    1.11  
    1.12 @@ -164,13 +164,13 @@
    1.13        ((structure.span_depth, structure.after_span_depth) /: tokens) {
    1.14          case ((x, y), tok) =>
    1.15            if (tok.is_command) {
    1.16 -            if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
    1.17 -            else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
    1.18 -            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
    1.19 -            else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
    1.20 -            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
    1.21 -            else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
    1.22 -            else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
    1.23 +            if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
    1.24 +            else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
    1.25 +            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
    1.26 +            else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
    1.27 +            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
    1.28 +            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    1.29 +            else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    1.30              else (x, y)
    1.31            }
    1.32            else (x, y)