equal
deleted
inserted
replaced
49 val theory_name = atom("theory name", _.is_name) |
49 val theory_name = atom("theory name", _.is_name) |
50 |
50 |
51 val keyword_kind = |
51 val keyword_kind = |
52 atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } |
52 atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } |
53 val keyword_decl = |
53 val keyword_decl = |
54 rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^ |
54 rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^ |
55 { case xs ~ y => xs.map((_, y)) } |
55 { case xs ~ y => xs.map((_, y)) } |
56 val keyword_decls = |
56 val keyword_decls = |
57 keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
57 keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
58 { case xs ~ yss => (xs :: yss).flatten } |
58 { case xs ~ yss => (xs :: yss).flatten } |
59 |
59 |