src/Pure/Thy/thy_header.scala
changeset 36956 21be4832c362
parent 36948 d2cdad45fd14
child 38149 3c380380beac
     1.1 --- a/src/Pure/Thy/thy_header.scala	Mon May 17 10:20:55 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Mon May 17 14:23:54 2010 +0200
     1.3 @@ -59,14 +59,14 @@
     1.4    def read(file: File): Header =
     1.5    {
     1.6      val token = lexicon.token(symbols, _ => false)
     1.7 -    val toks = new mutable.ListBuffer[Outer_Lex.Token]
     1.8 +    val toks = new mutable.ListBuffer[Token]
     1.9  
    1.10      def scan_to_begin(in: Reader[Char])
    1.11      {
    1.12        token(in) match {
    1.13          case lexicon.Success(tok, rest) =>
    1.14            toks += tok
    1.15 -          if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
    1.16 +          if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
    1.17              scan_to_begin(rest)
    1.18          case _ =>
    1.19        }
    1.20 @@ -74,7 +74,7 @@
    1.21      val reader = Scan.byte_reader(file)
    1.22      try { scan_to_begin(reader) } finally { reader.close }
    1.23  
    1.24 -    parse(commit(header), Outer_Lex.reader(toks.toList)) match {
    1.25 +    parse(commit(header), Token.reader(toks.toList)) match {
    1.26        case Success(result, _) => result
    1.27        case bad => error(bad.toString)
    1.28      }