227 |
227 |
228 |
228 |
229 (** outer syntax **) |
229 (** outer syntax **) |
230 |
230 |
231 val dest_decl : (bool * binding option * string) parser = |
231 val dest_decl : (bool * binding option * string) parser = |
232 Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- |
232 @{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false -- |
233 (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 |
233 (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ) --| @{keyword ")"} >> Parse.triple1 |
234 || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" |
234 || @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"} |
235 >> (fn t => (true,NONE,t)) |
235 >> (fn t => (true, NONE, t)) |
236 || Parse.typ >> (fn t => (false,NONE,t)) |
236 || Parse.typ >> (fn t => (false, NONE, t)) |
237 |
237 |
238 val cons_decl = |
238 val cons_decl = |
239 Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix |
239 Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix |
240 |
240 |
241 val domain_decl = |
241 val domain_decl = |
242 (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- |
242 (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- |
243 (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl) |
243 (@{keyword "="} |-- Parse.enum1 "|" cons_decl) |
244 |
244 |
245 val domains_decl = |
245 val domains_decl = |
246 Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false -- |
246 Scan.optional (@{keyword "("} |-- (@{keyword "unsafe"} >> K true) --| @{keyword ")"}) false -- |
247 Parse.and_list1 domain_decl |
247 Parse.and_list1 domain_decl |
248 |
248 |
249 fun mk_domain |
249 fun mk_domain |
250 (unsafe : bool, |
250 (unsafe : bool, |
251 doms : ((((string * string option) list * binding) * mixfix) * |
251 doms : ((((string * string option) list * binding) * mixfix) * |