1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Thy/thy_header.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Theory headers -- independent of outer syntax.
     1.8 +Static theory header information.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -51,11 +51,11 @@
    1.13      val keyword_kind =
    1.14        atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    1.15      val keyword_decl =
    1.16 -      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    1.17 -      { case x ~ y => (x, y) }
    1.18 -    val keywords =
    1.19 +      rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    1.20 +      { case xs ~ y => xs.map((_, y)) }
    1.21 +    val keyword_decls =
    1.22        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.23 -      { case x ~ ys => x :: ys }
    1.24 +      { case xs ~ yss => (xs :: yss).flatten }
    1.25  
    1.26      val file =
    1.27        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    1.28 @@ -64,7 +64,7 @@
    1.29      val args =
    1.30        theory_name ~
    1.31        (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
    1.32 -      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.33 +      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.34        (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.35        keyword(BEGIN) ^^
    1.36        { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }