src/Pure/Thy/thy_header.scala
changeset 51294 0850d43cb355
parent 51293 05b1bbae748d
child 51627 589daaf48dba
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Feb 27 12:45:19 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Feb 27 16:27:44 2013 +0100
     1.3 @@ -12,8 +12,6 @@
     1.4  import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.5  import scala.util.matching.Regex
     1.6  
     1.7 -import java.io.{File => JFile}
     1.8 -
     1.9  
    1.10  object Thy_Header extends Parse.Parser
    1.11  {
    1.12 @@ -72,7 +70,7 @@
    1.13        (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.14        (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.15        keyword(BEGIN) ^^
    1.16 -      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
    1.17 +      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    1.18  
    1.19      (keyword(HEADER) ~ tags) ~!
    1.20        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    1.21 @@ -117,10 +115,9 @@
    1.22  sealed case class Thy_Header(
    1.23    name: String,
    1.24    imports: List[String],
    1.25 -  keywords: Thy_Header.Keywords,
    1.26 -  files: List[String])
    1.27 +  keywords: Thy_Header.Keywords)
    1.28  {
    1.29    def map(f: String => String): Thy_Header =
    1.30 -    Thy_Header(f(name), imports.map(f), keywords, files.map(f))
    1.31 +    Thy_Header(f(name), imports.map(f), keywords)
    1.32  }
    1.33