diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Isar/token.scala Sun May 03 00:01:10 2015 +0200 @@ -144,7 +144,7 @@ var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.token_line(keywords, ctxt), in) match { - case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } + case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) } @@ -158,7 +158,7 @@ def implode(toks: List[Token]): String = toks match { case List(tok) => tok.source - case toks => toks.map(_.source).mkString + case _ => toks.map(_.source).mkString } @@ -222,7 +222,7 @@ } -sealed case class Token(val kind: Token.Kind.Value, val source: String) +sealed case class Token(kind: Token.Kind.Value, source: String) { def is_command: Boolean = kind == Token.Kind.COMMAND def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =