src/Pure/Thy/thy_header.scala
changeset 48864 3ee314ae1e0a
parent 48706 e2b512024eab
child 48882 61dc7d5d150a
     1.1 --- a/src/Pure/Thy/thy_header.scala	Mon Aug 20 13:58:06 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Aug 20 14:09:09 2012 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val BEGIN = "begin"
     1.5  
     1.6    private val lexicon =
     1.7 -    Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
     1.8 +    Scan.Lexicon("%", "(", ")", ",", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
     1.9  
    1.10  
    1.11    /* theory file name */
    1.12 @@ -47,10 +47,15 @@
    1.13    {
    1.14      val file_name = atom("file name", _.is_name)
    1.15  
    1.16 -    val keyword_kind =
    1.17 -      atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    1.18 +    val opt_files =
    1.19 +      keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
    1.20 +      success(Nil)
    1.21 +    val keyword_spec =
    1.22 +      atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    1.23 +      { case x ~ y ~ z => ((x, y), z) }
    1.24 +
    1.25      val keyword_decl =
    1.26 -      rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    1.27 +      rep1(string) ~ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    1.28        { case xs ~ y => xs.map((_, y)) }
    1.29      val keyword_decls =
    1.30        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.31 @@ -111,7 +116,7 @@
    1.32  
    1.33    /* keywords */
    1.34  
    1.35 -  type Keywords = List[(String, Option[(String, List[String])])]
    1.36 +  type Keywords = List[(String, Option[((String, List[String]), List[String])])]
    1.37  }
    1.38  
    1.39