src/Pure/Isar/outer_syntax.scala
changeset 59122 c1dbcde94cd2
parent 59083 88b0b1f28adc
child 59319 677615cba30d
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 09 20:00:45 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 09 21:14:11 2014 +0100
     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 => keywords.is_command_kind(tok, Keyword.theory))) 0
     1.8 +      if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
     1.9        else if (command1) struct.after_span_depth
    1.10        else struct.span_depth
    1.11  
    1.12 @@ -164,15 +164,15 @@
    1.13        ((struct.span_depth, struct.after_span_depth) /: tokens) {
    1.14          case ((x, y), tok) =>
    1.15            if (tok.is_command) {
    1.16 -            if (keywords.is_command_kind(tok, Keyword.theory_goal))
    1.17 +            if (tok.is_command_kind(keywords, Keyword.theory_goal))
    1.18                (2, 1)
    1.19 -            else if (keywords.is_command_kind(tok, Keyword.theory))
    1.20 +            else if (tok.is_command_kind(keywords, Keyword.theory))
    1.21                (1, 0)
    1.22 -            else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    1.23 +            else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
    1.24                (y + 2, y + 1)
    1.25 -            else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
    1.26 +            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
    1.27                (y + 1, y - 1)
    1.28 -            else if (keywords.is_command_kind(tok, Keyword.qed_global))
    1.29 +            else if (tok.is_command_kind(keywords, Keyword.qed_global))
    1.30                (1, 0)
    1.31              else (x, y)
    1.32            }