equal
deleted
inserted
replaced
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 }) ^^ |