src/Pure/Isar/outer_syntax.scala
changeset 63479 464ef556bd21
parent 63460 f41070510341
child 63528 0f39f59317c1
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:10:35 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:36:47 2016 +0200
     1.3 @@ -174,9 +174,9 @@
     1.4              if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
     1.5              else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
     1.6              else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
     1.7 -            else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
     1.8 -            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
     1.9 -            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
    1.10 +            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
    1.11 +            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
    1.12 +            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
    1.13              else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    1.14              else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    1.15              else (x, y)