src/Pure/Thy/thy_header.scala
changeset 55492 28d4db6c6e79
parent 51627 589daaf48dba
child 55494 009b71c1ed23
     1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Feb 14 14:52:50 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Feb 14 15:42:27 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 = lexicon.token(_ => false)
     1.8 +    val token = Scan.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 lexicon.Success(tok, rest) =>
    1.15 +        case Scan.Parsers.Success(tok, rest) =>
    1.16            toks += tok
    1.17            if (!tok.is_begin) scan_to_begin(rest)
    1.18          case _ =>