29 sig |
29 sig |
30 val clasetN: string |
30 val clasetN: string |
31 val clasetK: Object.kind |
31 val clasetK: Object.kind |
32 exception ClasetData of Object.T ref |
32 exception ClasetData of Object.T ref |
33 val setup: (theory -> theory) list |
33 val setup: (theory -> theory) list |
34 val fix_methods: Object.T * (Object.T -> Object.T) * |
34 val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) * |
35 (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit |
35 (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit |
36 end; |
36 end; |
37 |
37 |
38 signature CLASSICAL_DATA = |
38 signature CLASSICAL_DATA = |
39 sig |
39 sig |
179 |
179 |
180 local |
180 local |
181 fun undef _ = raise Match; |
181 fun undef _ = raise Match; |
182 |
182 |
183 val empty_ref = ref ERROR; |
183 val empty_ref = ref ERROR; |
|
184 val copy_fn = ref (undef: Object.T -> Object.T); |
184 val prep_ext_fn = ref (undef: Object.T -> Object.T); |
185 val prep_ext_fn = ref (undef: Object.T -> Object.T); |
185 val merge_fn = ref (undef: Object.T * Object.T -> Object.T); |
186 val merge_fn = ref (undef: Object.T * Object.T -> Object.T); |
186 val print_fn = ref (undef: Sign.sg -> Object.T -> unit); |
187 val print_fn = ref (undef: Sign.sg -> Object.T -> unit); |
187 |
188 |
188 val empty = ClasetData empty_ref; |
189 val empty = ClasetData empty_ref; |
|
190 fun copy exn = ! copy_fn exn; |
189 fun prep_ext exn = ! prep_ext_fn exn; |
191 fun prep_ext exn = ! prep_ext_fn exn; |
190 fun merge exn = ! merge_fn exn; |
192 fun merge exn = ! merge_fn exn; |
191 fun print sg exn = ! print_fn sg exn; |
193 fun print sg exn = ! print_fn sg exn; |
192 in |
194 in |
193 val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)]; |
195 val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)]; |
194 fun fix_methods (e, ext, mrg, prt) = |
196 fun fix_methods (e, cp, ext, mrg, prt) = |
195 (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt); |
197 (empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt); |
196 end; |
198 end; |
197 |
199 |
198 |
200 |
199 end; |
201 end; |
200 |
202 |
785 |
787 |
786 local |
788 local |
787 val empty = CSData (ref empty_cs); |
789 val empty = CSData (ref empty_cs); |
788 |
790 |
789 (*create new references*) |
791 (*create new references*) |
790 fun prep_ext (ClasetData (ref (CSData (ref cs)))) = |
792 fun copy (ClasetData (ref (CSData (ref cs)))) = |
791 ClasetData (ref (CSData (ref cs))); |
793 ClasetData (ref (CSData (ref cs))); |
|
794 val prep_ext = copy; |
792 |
795 |
793 fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) = |
796 fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) = |
794 ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); |
797 ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); |
795 |
798 |
796 fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs; |
799 fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs; |
797 in |
800 in |
798 val _ = fix_methods (empty, prep_ext, merge, print); |
801 val _ = fix_methods (empty, copy, prep_ext, merge, print); |
799 end; |
802 end; |
800 |
803 |
801 |
804 |
802 (* access claset *) |
805 (* access claset *) |
803 |
806 |