author | wenzelm |
Sat, 25 Jan 2014 16:46:39 +0100 | |
changeset 55137 | 6cac9fbf9b79 |
parent 55136 | fb10f6ce0c16 |
child 55138 | 2fa86fa27a0f |
--- a/src/Pure/Isar/token.scala Sat Jan 25 16:45:13 2014 +0100 +++ b/src/Pure/Isar/token.scala Sat Jan 25 16:46:39 2014 +0100 @@ -108,7 +108,7 @@ else source def text: (String, String) = - if (is_command && source == ";") ("terminator", "") + if (is_keyword && source == ";") ("terminator", "") else (kind.toString, source) }