13 end; |
13 end; |
14 |
14 |
15 signature ATTRIB = |
15 signature ATTRIB = |
16 sig |
16 sig |
17 include BASIC_ATTRIB |
17 include BASIC_ATTRIB |
18 val help_attributes: theory option -> unit |
18 val help_attributes: theory option -> Pretty.T list |
19 exception ATTRIB_FAIL of (string * Position.T) * exn |
19 exception ATTRIB_FAIL of (string * Position.T) * exn |
20 val global_attribute: theory -> Args.src -> theory attribute |
20 val global_attribute: theory -> Args.src -> theory attribute |
21 val local_attribute: theory -> Args.src -> Proof.context attribute |
21 val local_attribute: theory -> Args.src -> Proof.context attribute |
22 val local_attribute': Proof.context -> Args.src -> Proof.context attribute |
22 val local_attribute': Proof.context -> Args.src -> Proof.context attribute |
23 val undef_global_attribute: theory attribute |
23 val undef_global_attribute: theory attribute |
60 fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = |
60 fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = |
61 {space = NameSpace.merge (space1, space2), |
61 {space = NameSpace.merge (space1, space2), |
62 attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => |
62 attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => |
63 error ("Attempt to merge different versions of attributes " ^ commas_quote dups)}; |
63 error ("Attempt to merge different versions of attributes " ^ commas_quote dups)}; |
64 |
64 |
65 fun print_atts verbose ({space, attrs}) = |
65 fun pretty_atts verbose ({space, attrs}) = |
66 let |
66 let |
67 fun prt_attr (name, ((_, comment), _)) = Pretty.block |
67 fun prt_attr (name, ((_, comment), _)) = Pretty.block |
68 [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
68 [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
69 in |
69 in |
70 if not verbose then () |
70 (if not verbose then [] else [Display.pretty_name_space ("attribute name space", space)]) @ |
71 else Pretty.writeln (Display.pretty_name_space ("attribute name space", space)); |
71 [Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))] |
72 Pretty.writeln (Pretty.big_list "attributes:" |
|
73 (map prt_attr (NameSpace.cond_extern_table space attrs))) |
|
74 end; |
72 end; |
75 |
73 |
76 fun print _ = print_atts true; |
74 fun print _ = Pretty.writeln o Pretty.chunks o pretty_atts true; |
77 end; |
75 end; |
78 |
76 |
79 structure AttributesData = TheoryDataFun(AttributesDataArgs); |
77 structure AttributesData = TheoryDataFun(AttributesDataArgs); |
80 val print_attributes = AttributesData.print; |
78 val print_attributes = AttributesData.print; |
81 |
79 |
82 fun help_attributes None = writeln "attributes: (unkown theory context)" |
80 fun help_attributes None = [Pretty.str "attributes: (unkown theory context)"] |
83 | help_attributes (Some thy) = AttributesDataArgs.print_atts false (AttributesData.get thy); |
81 | help_attributes (Some thy) = AttributesDataArgs.pretty_atts false (AttributesData.get thy); |
84 |
82 |
85 |
83 |
86 (* get global / local attributes *) |
84 (* get global / local attributes *) |
87 |
85 |
88 exception ATTRIB_FAIL of (string * Position.T) * exn; |
86 exception ATTRIB_FAIL of (string * Position.T) * exn; |