src/Pure/Isar/parse.scala

 
 import scala.util.parsing.combinator.Parsers
 import scala.annotation.tailrec
 
 
-object Parse
-{
+object Parse {
   /* parsing tokens */
 
-  trait Parser extends Parsers
-  {
+  trait Parser extends Parsers {
     type Elem = Token
 
     def filter_proper: Boolean = true
 
     @tailrec private def proper(in: Input): Input =
       if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
     private def proper_position: Parser[Position.T] =
       new Parser[Position.T] {
-        def apply(raw_input: Input) =
-        {
+        def apply(raw_input: Input) = {
           val in = proper(raw_input)
           val pos =
             in.pos match {
               case pos: Token.Pos => pos
               case _ => Token.Pos.none

     def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
       proper_position ~ parser ^^ { case x ~ y => (y, x) }
 
     def token(s: String, pred: Elem => Boolean): Parser[Elem] =
       new Parser[Elem] {
-        def apply(raw_input: Input) =
-        {
+        def apply(raw_input: Input) = {
           val in = proper(raw_input)
           if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
           else {
             val token = in.first
             if (pred(token)) Success(token, proper(in.rest))

 
     /* wrappers */
 
     def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
 
-    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] =
-    {
+    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = {
       val result = parse(p, in)
       val rest = proper(result.next)
       if (result.successful && !rest.atEnd) Error("bad input", rest)
       else result
     }