src/Pure/Thy/thy_header.scala
changeset 46938 cda018294515
parent 46737 09ab89658a5d
child 46939 5b67ac48b384
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Mar 14 22:34:18 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
     1.3 @@ -20,10 +20,13 @@
     1.4    val HEADER = "header"
     1.5    val THEORY = "theory"
     1.6    val IMPORTS = "imports"
     1.7 +  val KEYWORDS = "keywords"
     1.8 +  val AND = "and"
     1.9    val USES = "uses"
    1.10    val BEGIN = "begin"
    1.11  
    1.12 -  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
    1.13 +  private val lexicon =
    1.14 +    Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
    1.15  
    1.16  
    1.17    /* theory file name */
    1.18 @@ -45,15 +48,26 @@
    1.19      val file_name = atom("file name", _.is_name)
    1.20      val theory_name = atom("theory name", _.is_name)
    1.21  
    1.22 +    val keyword_kind =
    1.23 +      atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    1.24 +    val keyword_decl =
    1.25 +      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    1.26 +      { case x ~ y => (x, y) }
    1.27 +    val keywords =
    1.28 +      keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.29 +      { case x ~ ys => x :: ys }
    1.30 +
    1.31      val file =
    1.32        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    1.33        file_name ^^ (x => (x, true))
    1.34  
    1.35 -    val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
    1.36 -
    1.37      val args =
    1.38 -      theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
    1.39 -        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
    1.40 +      theory_name ~
    1.41 +      (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
    1.42 +      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.43 +      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.44 +      keyword(BEGIN) ^^
    1.45 +      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
    1.46  
    1.47      (keyword(HEADER) ~ tags) ~!
    1.48        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    1.49 @@ -98,9 +112,11 @@
    1.50  
    1.51  
    1.52  sealed case class Thy_Header(
    1.53 -  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
    1.54 +  name: String, imports: List[String],
    1.55 +  keywords: List[(String, Option[(String, List[String])])],
    1.56 +  uses: List[(String, Boolean)])
    1.57  {
    1.58    def map(f: String => String): Thy_Header =
    1.59 -    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
    1.60 +    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
    1.61  }
    1.62