1.1 --- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 00:10:45 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 09:55:42 2012 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Thy/thy_header.ML
     1.5 -    Author:     Markus Wenzel, TU Muenchen
     1.6 +    Author:     Makarius
     1.7  
     1.8 -Theory headers -- independent of outer syntax.
     1.9 +Static theory header information.
    1.10  *)
    1.11  
    1.12  signature THY_HEADER =
    1.13 @@ -80,7 +80,10 @@
    1.14  val theory_name = Parse.group (fn () => "theory name") Parse.name;
    1.15  
    1.16  val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
    1.17 -val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind);
    1.18 +val keyword_decl =
    1.19 +  Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
    1.20 +  (fn (names, kind) => map (rpair kind) names);
    1.21 +val keyword_decls = Parse.and_list1 keyword_decl >> flat;
    1.22  
    1.23  val file =
    1.24    Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
    1.25 @@ -91,7 +94,7 @@
    1.26  val args =
    1.27    theory_name --
    1.28    (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
    1.29 -  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] --
    1.30 +  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --
    1.31    Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
    1.32    Parse.$$$ beginN >>
    1.33    (fn (((name, imports), keywords), uses) => make name imports keywords uses);

     2.1 --- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Pure/Thy/thy_header.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Theory headers -- independent of outer syntax.
     2.8 +Static theory header information.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12 @@ -51,11 +51,11 @@
    2.13      val keyword_kind =
    2.14        atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    2.15      val keyword_decl =
    2.16 -      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    2.17 -      { case x ~ y => (x, y) }
    2.18 -    val keywords =
    2.19 +      rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    2.20 +      { case xs ~ y => xs.map((_, y)) }
    2.21 +    val keyword_decls =
    2.22        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    2.23 -      { case x ~ ys => x :: ys }
    2.24 +      { case xs ~ yss => (xs :: yss).flatten }
    2.25  
    2.26      val file =
    2.27        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    2.28 @@ -64,7 +64,7 @@
    2.29      val args =
    2.30        theory_name ~
    2.31        (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
    2.32 -      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    2.33 +      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    2.34        (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    2.35        keyword(BEGIN) ^^
    2.36        { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }