17 val intern: theory -> xstring -> string |
17 val intern: theory -> xstring -> string |
18 val intern_src: theory -> src -> src |
18 val intern_src: theory -> src -> src |
19 val pretty_attribs: Proof.context -> src list -> Pretty.T list |
19 val pretty_attribs: Proof.context -> src list -> Pretty.T list |
20 val attribute: theory -> src -> attribute |
20 val attribute: theory -> src -> attribute |
21 val attribute_i: theory -> src -> attribute |
21 val attribute_i: theory -> src -> attribute |
22 val eval_thms: Proof.context -> (thmref * src list) list -> thm list |
22 val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list |
23 val map_specs: ('a -> 'att) -> |
23 val map_specs: ('a -> 'att) -> |
24 (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list |
24 (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list |
25 val map_facts: ('a -> 'att) -> |
25 val map_facts: ('a -> 'att) -> |
26 (('c * 'a list) * ('d * 'a list) list) list -> |
26 (('c * 'a list) * ('d * 'a list) list) list -> |
27 (('c * 'att list) * ('d * 'att list) list) list |
27 (('c * 'att list) * ('d * 'att list) list) list |
155 |
155 |
156 (** parsing attributed theorems **) |
156 (** parsing attributed theorems **) |
157 |
157 |
158 local |
158 local |
159 |
159 |
160 val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms; |
|
161 |
|
162 val fact_name = Args.internal_fact >> K "<fact>" || Args.name; |
160 val fact_name = Args.internal_fact >> K "<fact>" || Args.name; |
163 |
161 |
164 fun gen_thm pick = Scan.depend (fn st => |
162 fun gen_thm pick = Scan.depend (fn context => |
165 Args.$$$ "[" |-- Args.attribs (intern (Context.theory_of st)) --| Args.$$$ "]" |
163 let |
166 >> (fn srcs => |
164 val thy = Context.theory_of context; |
|
165 val get = Context.cases PureThy.get_thms ProofContext.get_thms context; |
|
166 fun get_fact s = get (Facts.Fact s); |
|
167 fun get_named s = get (Facts.Named (s, NONE)); |
|
168 in |
|
169 Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs => |
167 let |
170 let |
168 val atts = map (attribute_i (Context.theory_of st)) srcs; |
171 val atts = map (attribute_i thy) srcs; |
169 val (st', th') = Library.apply atts (st, Drule.dummy_thm); |
172 val (context', th') = Library.apply atts (context, Drule.dummy_thm); |
170 in (st', pick "" [th']) end) || |
173 in (context', pick "" [th']) end) |
171 (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact) |
174 || |
172 >> (fn (s, fact) => ("", Fact s, fact)) || |
175 (Scan.ahead Args.alt_name -- Args.named_fact get_fact |
173 Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel |
176 >> (fn (s, fact) => ("", Facts.Fact s, fact)) |
174 >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) || |
177 || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel |
175 Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) |
178 >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact))) |
176 >> (fn (name, fact) => (name, Name name, fact))) |
179 -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) => |
177 -- Args.opt_attribs (intern (Context.theory_of st)) |
180 let |
178 >> (fn ((name, thmref, fact), srcs) => |
181 val ths = Facts.select thmref fact; |
179 let |
182 val atts = map (attribute_i thy) srcs; |
180 val ths = PureThy.select_thm thmref fact; |
183 val (context', ths') = foldl_map (Library.apply atts) (context, ths); |
181 val atts = map (attribute_i (Context.theory_of st)) srcs; |
184 in (context', pick name ths') end) |
182 val (st', ths') = foldl_map (Library.apply atts) (st, ths); |
185 end); |
183 in (st', pick name ths') end)); |
|
184 |
186 |
185 in |
187 in |
186 |
188 |
187 val thm = gen_thm PureThy.single_thm; |
189 val thm = gen_thm Facts.the_single; |
188 val multi_thm = gen_thm (K I); |
190 val multi_thm = gen_thm (K I); |
189 val thms = Scan.repeat multi_thm >> flat; |
191 val thms = Scan.repeat multi_thm >> flat; |
190 |
192 |
191 end; |
193 end; |
192 |
194 |