equal
deleted
inserted
replaced
136 val keyword_decls = |
136 val keyword_decls = |
137 keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
137 keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
138 { case xs ~ yss => (xs :: yss).flatten } |
138 { case xs ~ yss => (xs :: yss).flatten } |
139 |
139 |
140 val abbrevs = |
140 val abbrevs = |
141 rep1sep(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }, $$$("and")) |
141 rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^ |
|
142 { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) } |
142 |
143 |
143 val args = |
144 val args = |
144 position(theory_name) ~ |
145 position(theory_name) ~ |
145 (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ |
146 (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ |
146 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
147 { case None => Nil case Some(_ ~ xs) => xs }) ~ |