src/Pure/Thy/thy_header.scala
changeset 55494 009b71c1ed23
parent 55492 28d4db6c6e79
child 56801 8dd9df88f647
     1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Feb 14 16:11:14 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Feb 14 16:25:30 2014 +0100
     1.3 @@ -82,13 +82,13 @@
     1.4  
     1.5    def read(reader: Reader[Char]): Thy_Header =
     1.6    {
     1.7 -    val token = Scan.Parsers.token(lexicon, _ => false)
     1.8 +    val token = Token.Parsers.token(lexicon, _ => false)
     1.9      val toks = new mutable.ListBuffer[Token]
    1.10  
    1.11      @tailrec def scan_to_begin(in: Reader[Char])
    1.12      {
    1.13        token(in) match {
    1.14 -        case Scan.Parsers.Success(tok, rest) =>
    1.15 +        case Token.Parsers.Success(tok, rest) =>
    1.16            toks += tok
    1.17            if (!tok.is_begin) scan_to_begin(rest)
    1.18          case _ =>