src/Pure/Thy/thy_header.scala
changeset 58899 0a793c580685
parent 58868 c5e1cce7ace3
child 58900 1435cc20b022
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Nov 04 18:19:38 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 15:32:11 2014 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5    def read(reader: Reader[Char]): Thy_Header =
     1.6    {
     1.7 -    val token = Token.Parsers.token(lexicon, _ => false)
     1.8 +    val token = Token.Parsers.token(lexicon, Scan.Lexicon.empty)
     1.9      val toks = new mutable.ListBuffer[Token]
    1.10  
    1.11      @tailrec def scan_to_begin(in: Reader[Char])
    1.12 @@ -138,7 +138,7 @@
    1.13      val f = Symbol.decode _
    1.14      Thy_Header(f(name), imports.map(f),
    1.15        keywords.map({ case (a, b, c) =>
    1.16 -        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f))  }), c.map(f)) }))
    1.17 +        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
    1.18    }
    1.19  }
    1.20