src/Pure/Thy/thy_header.scala
changeset 48484 70898d016538
parent 48409 0d2114eb412a
child 48638 22d65e375c01
equal deleted inserted replaced
48483:9bfb6978eb80 48484:70898d016538
    44   /* header */
    44   /* header */
    45 
    45 
    46   val header: Parser[Thy_Header] =
    46   val header: Parser[Thy_Header] =
    47   {
    47   {
    48     val file_name = atom("file name", _.is_name)
    48     val file_name = atom("file name", _.is_name)
    49     val theory_name = atom("theory name", _.is_name)
       
    50 
    49 
    51     val keyword_kind =
    50     val keyword_kind =
    52       atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    51       atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
    53     val keyword_decl =
    52     val keyword_decl =
    54       rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
    53       rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^