src/Pure/Thy/thy_header.scala
changeset 51293 05b1bbae748d
parent 50128 599c935aac82
child 51294 0850d43cb355
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Feb 26 20:11:11 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Feb 27 12:45:19 2013 +0100
     1.3 @@ -22,12 +22,11 @@
     1.4    val IMPORTS = "imports"
     1.5    val KEYWORDS = "keywords"
     1.6    val AND = "and"
     1.7 -  val USES = "uses"
     1.8    val BEGIN = "begin"
     1.9  
    1.10    private val lexicon =
    1.11      Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
    1.12 -      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
    1.13 +      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
    1.14  
    1.15  
    1.16    /* theory file name */
    1.17 @@ -72,9 +71,8 @@
    1.18        theory_name ~
    1.19        (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.20        (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.21 -      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.22        keyword(BEGIN) ^^
    1.23 -      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
    1.24 +      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
    1.25  
    1.26      (keyword(HEADER) ~ tags) ~!
    1.27        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    1.28 @@ -120,9 +118,9 @@
    1.29    name: String,
    1.30    imports: List[String],
    1.31    keywords: Thy_Header.Keywords,
    1.32 -  uses: List[(String, Boolean)])
    1.33 +  files: List[String])
    1.34  {
    1.35    def map(f: String => String): Thy_Header =
    1.36 -    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
    1.37 +    Thy_Header(f(name), imports.map(f), keywords, files.map(f))
    1.38  }
    1.39