equal
deleted
inserted
replaced
144 |
144 |
145 (** outer syntax **) |
145 (** outer syntax **) |
146 |
146 |
147 local structure P = OuterParse and K = OuterKeyword in |
147 local structure P = OuterParse and K = OuterKeyword in |
148 |
148 |
|
149 val _ = OuterSyntax.keywords ["lazy"]; |
|
150 |
149 val dest_decl = |
151 val dest_decl = |
150 P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
152 P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
151 (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 |
153 (P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 |
152 || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" |
154 || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" |
153 >> (fn t => (true,NONE,t)) |
155 >> (fn t => (true,NONE,t)) |
168 val domains_decl = |
170 val domains_decl = |
169 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
171 Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl |
170 >> (fn (opt_name, doms) => |
172 >> (fn (opt_name, doms) => |
171 (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); |
173 (case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms)); |
172 |
174 |
173 val domainP = |
175 val _ = |
174 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
176 OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl |
175 (domains_decl >> (Toplevel.theory o add_domain)); |
177 (domains_decl >> (Toplevel.theory o add_domain)); |
176 |
178 |
177 |
179 end; |
178 val _ = OuterSyntax.add_keywords ["lazy"]; |
|
179 val _ = OuterSyntax.add_parsers [domainP]; |
|
180 |
|
181 end; (* local structure *) |
|
182 |
180 |
183 end; |
181 end; |