author | wenzelm |
Tue, 27 Nov 2018 21:07:39 +0100 | |
changeset 69349 | 7cef9e386ffe |
parent 69216 | 1a52baa70aed |
child 69575 | f77cc54f6d47 |
permissions | -rw-r--r-- |
5823 | 1 |
(* Title: Pure/Isar/attrib.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
18734 | 4 |
Symbolic representation of attributes -- with name and syntax. |
5823 | 5 |
*) |
6 |
||
7 |
signature ATTRIB = |
|
8 |
sig |
|
67652 | 9 |
type thms = Attrib.thms |
10 |
type fact = Attrib.fact |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
11 |
val print_attributes: bool -> Proof.context -> unit |
63336 | 12 |
val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory |
13 |
val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
14 |
val check_name_generic: Context.generic -> xstring * Position.T -> string |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
15 |
val check_name: Proof.context -> xstring * Position.T -> string |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
16 |
val check_src: Proof.context -> Token.src -> Token.src |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
17 |
val attribs: Token.src list context_parser |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
18 |
val opt_attribs: Token.src list context_parser |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
19 |
val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list |
63336 | 20 |
val pretty_binding: Proof.context -> Attrib.binding -> string -> Pretty.T list |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
21 |
val attribute: Proof.context -> Token.src -> attribute |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
22 |
val attribute_global: theory -> Token.src -> attribute |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
23 |
val attribute_cmd: Proof.context -> Token.src -> attribute |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
24 |
val attribute_cmd_global: theory -> Token.src -> attribute |
45390
e29521ef9059
tuned signature -- avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45375
diff
changeset
|
25 |
val map_specs: ('a list -> 'att list) -> |
30759 | 26 |
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list |
45390
e29521ef9059
tuned signature -- avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45375
diff
changeset
|
27 |
val map_facts: ('a list -> 'att list) -> |
17105
1b07a176a880
added map_specs/facts operators (from locale.ML);
wenzelm
parents:
16934
diff
changeset
|
28 |
(('c * 'a list) * ('d * 'a list) list) list -> |
18905 | 29 |
(('c * 'att list) * ('d * 'att list) list) list |
45390
e29521ef9059
tuned signature -- avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45375
diff
changeset
|
30 |
val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) -> |
30759 | 31 |
(('c * 'a list) * ('b * 'a list) list) list -> |
32 |
(('c * 'att list) * ('fact * 'att list) list) list |
|
67652 | 33 |
val trim_context_binding: Attrib.binding -> Attrib.binding |
34 |
val trim_context_thms: thms -> thms |
|
35 |
val trim_context_fact: fact -> fact |
|
36 |
val global_notes: string -> fact list -> theory -> |
|
37 |
(string * thm list) list * theory |
|
38 |
val local_notes: string -> fact list -> Proof.context -> |
|
39 |
(string * thm list) list * Proof.context |
|
40 |
val generic_notes: string -> fact list -> Context.generic -> |
|
41 |
(string * thm list) list * Context.generic |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67652
diff
changeset
|
42 |
val lazy_notes: string -> binding * thm list lazy -> Context.generic -> Context.generic |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
43 |
val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
44 |
val attribute_syntax: attribute context_parser -> Token.src -> attribute |
63336 | 45 |
val setup: binding -> attribute context_parser -> string -> theory -> theory |
46 |
val local_setup: binding -> attribute context_parser -> string -> |
|
57927 | 47 |
local_theory -> local_theory |
59064 | 48 |
val attribute_setup: bstring * Position.T -> Input.source -> string -> |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
49 |
local_theory -> local_theory |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
50 |
val internal: (morphism -> attribute) -> Token.src |
63267 | 51 |
val internal_declaration: declaration -> thms |
30525
8a5a0aa30e1c
added setup and attribute_setup -- expect plain parser instead of syntax function;
wenzelm
parents:
30513
diff
changeset
|
52 |
val add_del: attribute -> attribute -> attribute context_parser |
30513 | 53 |
val thm: thm context_parser |
54 |
val thms: thm list context_parser |
|
55 |
val multi_thm: thm list context_parser |
|
67652 | 56 |
val transform_facts: morphism -> fact list -> fact list |
57 |
val partial_evaluation: Proof.context -> fact list -> fact list |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
58 |
val print_options: bool -> Proof.context -> unit |
63336 | 59 |
val config_bool: binding -> (Context.generic -> bool) -> bool Config.T * (theory -> theory) |
60 |
val config_int: binding -> (Context.generic -> int) -> int Config.T * (theory -> theory) |
|
61 |
val config_real: binding -> (Context.generic -> real) -> real Config.T * (theory -> theory) |
|
62 |
val config_string: binding -> (Context.generic -> string) -> string Config.T * (theory -> theory) |
|
63 |
val setup_config_bool: binding -> (Context.generic -> bool) -> bool Config.T |
|
64 |
val setup_config_int: binding -> (Context.generic -> int) -> int Config.T |
|
65 |
val setup_config_real: binding -> (Context.generic -> real) -> real Config.T |
|
66 |
val setup_config_string: binding -> (Context.generic -> string) -> string Config.T |
|
56438 | 67 |
val option_bool: string * Position.T -> bool Config.T * (theory -> theory) |
68 |
val option_int: string * Position.T -> int Config.T * (theory -> theory) |
|
69 |
val option_real: string * Position.T -> real Config.T * (theory -> theory) |
|
70 |
val option_string: string * Position.T -> string Config.T * (theory -> theory) |
|
71 |
val setup_option_bool: string * Position.T -> bool Config.T |
|
72 |
val setup_option_int: string * Position.T -> int Config.T |
|
73 |
val setup_option_real: string * Position.T -> real Config.T |
|
74 |
val setup_option_string: string * Position.T -> string Config.T |
|
63019 | 75 |
val consumes: int -> Token.src |
76 |
val constraints: int -> Token.src |
|
77 |
val cases_open: Token.src |
|
78 |
val case_names: string list -> Token.src |
|
79 |
val case_conclusion: string * string list -> Token.src |
|
5823 | 80 |
end; |
81 |
||
63336 | 82 |
structure Attrib: sig type binding = Attrib.binding include ATTRIB end = |
5823 | 83 |
struct |
84 |
||
67652 | 85 |
open Attrib; |
45584
41a768a431a6
do not store vacuous theorem specifications -- relevant for frugal local theory content;
wenzelm
parents:
45537
diff
changeset
|
86 |
|
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
87 |
|
27729 | 88 |
|
18734 | 89 |
(** named attributes **) |
18636 | 90 |
|
18734 | 91 |
(* theory data *) |
5823 | 92 |
|
57927 | 93 |
structure Attributes = Generic_Data |
22846 | 94 |
( |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
95 |
type T = ((Token.src -> attribute) * string) Name_Space.table; |
33159 | 96 |
val empty : T = Name_Space.empty_table "attribute"; |
16458 | 97 |
val extend = I; |
33522 | 98 |
fun merge data : T = Name_Space.merge_tables data; |
22846 | 99 |
); |
5823 | 100 |
|
63090
7aa9ac5165e4
common entity definitions within a global or local theory context;
wenzelm
parents:
63068
diff
changeset
|
101 |
val ops_attributes = {get_data = Attributes.get, put_data = Attributes.put}; |
57927 | 102 |
|
63090
7aa9ac5165e4
common entity definitions within a global or local theory context;
wenzelm
parents:
63068
diff
changeset
|
103 |
val get_attributes = Attributes.get o Context.Proof; |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
104 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
105 |
fun print_attributes verbose ctxt = |
22846 | 106 |
let |
57927 | 107 |
val attribs = get_attributes ctxt; |
50301 | 108 |
fun prt_attr (name, (_, "")) = Pretty.mark_str name |
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42808
diff
changeset
|
109 |
| prt_attr (name, (_, comment)) = |
50301 | 110 |
Pretty.block |
111 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
22846 | 112 |
in |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
113 |
[Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))] |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56303
diff
changeset
|
114 |
|> Pretty.writeln_chunks |
22846 | 115 |
end; |
7611 | 116 |
|
57927 | 117 |
val attribute_space = Name_Space.space_of_table o get_attributes; |
118 |
||
119 |
||
120 |
(* define *) |
|
121 |
||
63090
7aa9ac5165e4
common entity definitions within a global or local theory context;
wenzelm
parents:
63068
diff
changeset
|
122 |
fun define_global binding att comment = |
7aa9ac5165e4
common entity definitions within a global or local theory context;
wenzelm
parents:
63068
diff
changeset
|
123 |
Entity.define_global ops_attributes binding (att, comment); |
56027
25889f5c39a8
prefer Name_Space.pretty with its builtin markup;
wenzelm
parents:
56026
diff
changeset
|
124 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
125 |
fun define binding att comment = |
63090
7aa9ac5165e4
common entity definitions within a global or local theory context;
wenzelm
parents:
63068
diff
changeset
|
126 |
Entity.define ops_attributes binding (att, comment); |
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31305
diff
changeset
|
127 |
|
5823 | 128 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
129 |
(* check *) |
15703 | 130 |
|
57927 | 131 |
fun check_name_generic context = #1 o Name_Space.check context (Attributes.get context); |
56032
b034b9f0fa2a
clarified Args.check_src: retain name space information for error output;
wenzelm
parents:
56029
diff
changeset
|
132 |
val check_name = check_name_generic o Context.Proof; |
15703 | 133 |
|
56033 | 134 |
fun check_src ctxt src = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
135 |
let |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
136 |
val _ = |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
137 |
if Token.checked_src src then () |
62795
063d2f23cdf6
removed redundant Position.set_range -- already done in Position.range;
wenzelm
parents:
62498
diff
changeset
|
138 |
else Context_Position.report ctxt (#1 (Token.range_of src)) Markup.language_attribute; |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
139 |
in #1 (Token.check_src ctxt get_attributes src) end; |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
140 |
|
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
141 |
val attribs = |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
142 |
Args.context -- Scan.lift Parse.attribs |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
143 |
>> (fn (ctxt, srcs) => map (check_src ctxt) srcs); |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
144 |
|
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
145 |
val opt_attribs = Scan.optional attribs []; |
21031 | 146 |
|
147 |
||
148 |
(* pretty printing *) |
|
149 |
||
150 |
fun pretty_attribs _ [] = [] |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
151 |
| pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)]; |
21031 | 152 |
|
60242
3a8501876dba
tuned output -- avoid empty quites and extra breaks;
wenzelm
parents:
59917
diff
changeset
|
153 |
fun pretty_binding ctxt (b, atts) sep = |
60243 | 154 |
(case (Binding.is_empty b, null atts) of |
155 |
(true, true) => [] |
|
156 |
| (false, true) => [Pretty.block [Binding.pretty b, Pretty.str sep]] |
|
157 |
| (true, false) => [Pretty.block (pretty_attribs ctxt atts @ [Pretty.str sep])] |
|
158 |
| (false, false) => |
|
159 |
[Pretty.block |
|
160 |
(Binding.pretty b :: Pretty.brk 1 :: pretty_attribs ctxt atts @ [Pretty.str sep])]); |
|
60242
3a8501876dba
tuned output -- avoid empty quites and extra breaks;
wenzelm
parents:
59917
diff
changeset
|
161 |
|
15703 | 162 |
|
18734 | 163 |
(* get attributes *) |
5823 | 164 |
|
47816
cd0dfb06b0c8
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
wenzelm
parents:
47815
diff
changeset
|
165 |
fun attribute_generic context = |
57927 | 166 |
let val table = Attributes.get context |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
167 |
in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; |
5823 | 168 |
|
47816
cd0dfb06b0c8
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
wenzelm
parents:
47815
diff
changeset
|
169 |
val attribute = attribute_generic o Context.Proof; |
cd0dfb06b0c8
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
wenzelm
parents:
47815
diff
changeset
|
170 |
val attribute_global = attribute_generic o Context.Theory; |
47815 | 171 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55914
diff
changeset
|
172 |
fun attribute_cmd ctxt = attribute ctxt o check_src ctxt; |
56032
b034b9f0fa2a
clarified Args.check_src: retain name space information for error output;
wenzelm
parents:
56029
diff
changeset
|
173 |
fun attribute_cmd_global thy = attribute_global thy o check_src (Proof_Context.init_global thy); |
18636 | 174 |
|
5823 | 175 |
|
17105
1b07a176a880
added map_specs/facts operators (from locale.ML);
wenzelm
parents:
16934
diff
changeset
|
176 |
(* attributed declarations *) |
1b07a176a880
added map_specs/facts operators (from locale.ML);
wenzelm
parents:
16934
diff
changeset
|
177 |
|
45390
e29521ef9059
tuned signature -- avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45375
diff
changeset
|
178 |
fun map_specs f = map (apfst (apsnd f)); |
30759 | 179 |
|
45390
e29521ef9059
tuned signature -- avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45375
diff
changeset
|
180 |
fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f))); |
30759 | 181 |
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g))); |
17105
1b07a176a880
added map_specs/facts operators (from locale.ML);
wenzelm
parents:
16934
diff
changeset
|
182 |
|
1b07a176a880
added map_specs/facts operators (from locale.ML);
wenzelm
parents:
16934
diff
changeset
|
183 |
|
38330 | 184 |
(* fact expressions *) |
185 |
||
67652 | 186 |
val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src); |
187 |
val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context; |
|
188 |
fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms); |
|
67624 | 189 |
|
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
190 |
fun global_notes kind facts thy = thy |> |
47815 | 191 |
Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts); |
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
192 |
|
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
193 |
fun local_notes kind facts ctxt = ctxt |> |
47815 | 194 |
Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts); |
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
195 |
|
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
196 |
fun generic_notes kind facts context = context |> |
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
197 |
Context.mapping_result (global_notes kind facts) (local_notes kind facts); |
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47005
diff
changeset
|
198 |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67652
diff
changeset
|
199 |
fun lazy_notes kind arg = |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67652
diff
changeset
|
200 |
Context.mapping (Global_Theory.add_thms_lazy kind arg) (Proof_Context.add_thms_lazy kind arg); |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67652
diff
changeset
|
201 |
|
38330 | 202 |
fun eval_thms ctxt srcs = ctxt |
42360 | 203 |
|> Proof_Context.note_thmss "" |
63352 | 204 |
(map_facts_refs |
205 |
(map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) [(Binding.empty_atts, srcs)]) |
|
38330 | 206 |
|> fst |> maps snd; |
207 |
||
208 |
||
30525
8a5a0aa30e1c
added setup and attribute_setup -- expect plain parser instead of syntax function;
wenzelm
parents:
30513
diff
changeset
|
209 |
(* attribute setup *) |
8a5a0aa30e1c
added setup and attribute_setup -- expect plain parser instead of syntax function;
wenzelm
parents:
30513
diff
changeset
|
210 |
|
57927 | 211 |
fun attribute_syntax scan src (context, th) = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
212 |
let val (a, context') = Token.syntax_generic scan src context in a (context', th) end; |
57927 | 213 |
|
214 |
fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; |
|
215 |
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; |
|
5879 | 216 |
|
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
217 |
fun attribute_setup binding source comment = |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
218 |
ML_Context.expression (Input.pos_of source) |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
219 |
(ML_Lex.read |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
220 |
("Theory.local_setup (Attrib.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @ |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69187
diff
changeset
|
221 |
ML_Lex.read_source source @ ML_Lex.read (") " ^ ML_Syntax.print_string comment ^ ")")) |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
222 |
|> Context.proof_map; |
30525
8a5a0aa30e1c
added setup and attribute_setup -- expect plain parser instead of syntax function;
wenzelm
parents:
30513
diff
changeset
|
223 |
|
8a5a0aa30e1c
added setup and attribute_setup -- expect plain parser instead of syntax function;
wenzelm
parents:
30513
diff
changeset
|
224 |
|
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
225 |
(* internal attribute *) |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
226 |
|
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
227 |
val _ = Theory.setup |
64556 | 228 |
(setup (Binding.make ("attribute", \<^here>)) |
56436 | 229 |
(Scan.lift Args.internal_attribute >> Morphism.form) |
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
230 |
"internal attribute"); |
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
231 |
|
63019 | 232 |
fun internal_name ctxt name = |
233 |
Token.make_src (name, Position.none) [] |> check_src ctxt |> hd; |
|
234 |
||
235 |
val internal_attribute_name = |
|
236 |
internal_name (Context.the_local_context ()) "attribute"; |
|
237 |
||
238 |
fun internal att = |
|
239 |
internal_attribute_name :: |
|
240 |
[Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))]; |
|
241 |
||
63266 | 242 |
fun internal_declaration decl = |
243 |
[([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])]; |
|
244 |
||
55140
7eb0c04e4c40
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
wenzelm
parents:
53171
diff
changeset
|
245 |
|
31305 | 246 |
(* add/del syntax *) |
5823 | 247 |
|
31305 | 248 |
fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add); |
5879 | 249 |
|
250 |
||
25983 | 251 |
|
252 |
(** parsing attributed theorems **) |
|
5879 | 253 |
|
18636 | 254 |
local |
255 |
||
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
69216
diff
changeset
|
256 |
val fact_name = |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
69216
diff
changeset
|
257 |
Parse.position Args.internal_fact >> (fn (_, pos) => ("<fact>", pos)) || Args.name_position; |
21698
43a842769765
thms etc.: proper treatment of internal_fact with selection;
wenzelm
parents:
21658
diff
changeset
|
258 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
259 |
fun gen_thm pick = Scan.depend (fn context => |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
260 |
let |
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56052
diff
changeset
|
261 |
val get = Proof_Context.get_fact_generic context; |
26361 | 262 |
val get_fact = get o Facts.Fact; |
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57941
diff
changeset
|
263 |
fun get_named is_sel pos name = |
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57941
diff
changeset
|
264 |
let val (a, ths) = get (Facts.Named ((name, pos), NONE)) |
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57941
diff
changeset
|
265 |
in (if is_sel then NONE else a, ths) end; |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
266 |
in |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
267 |
Parse.$$$ "[" |-- Scan.pass context attribs --| Parse.$$$ "]" >> (fn srcs => |
24008 | 268 |
let |
47815 | 269 |
val atts = map (attribute_generic context) srcs; |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
46512
diff
changeset
|
270 |
val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context); |
55740 | 271 |
in (context', pick ("", Position.none) [th']) end) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
272 |
|| |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
273 |
(Scan.ahead Args.alt_name -- Args.named_fact get_fact |
27820 | 274 |
>> (fn (s, fact) => ("", Facts.Fact s, fact)) || |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
69216
diff
changeset
|
275 |
Scan.ahead (fact_name -- Scan.option Parse.thm_sel) :|-- |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
276 |
(fn ((name, pos), sel) => |
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
277 |
Args.named_fact (get_named (is_some sel) pos) --| Scan.option Parse.thm_sel |
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
278 |
>> (fn fact => (name, Facts.Named ((name, pos), sel), fact)))) |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
279 |
-- Scan.pass context opt_attribs >> (fn ((name, thmref, fact), srcs) => |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
280 |
let |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
281 |
val ths = Facts.select thmref fact; |
47815 | 282 |
val atts = map (attribute_generic context) srcs; |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
46512
diff
changeset
|
283 |
val (ths', context') = |
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
46512
diff
changeset
|
284 |
fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; |
55740 | 285 |
in (context', pick (name, Facts.pos_of_ref thmref) ths') end) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
286 |
end); |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset
|
287 |
|
18636 | 288 |
in |
289 |
||
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25983
diff
changeset
|
290 |
val thm = gen_thm Facts.the_single; |
18998 | 291 |
val multi_thm = gen_thm (K I); |
61476 | 292 |
val thms = Scan.repeats multi_thm; |
18636 | 293 |
|
294 |
end; |
|
295 |
||
5823 | 296 |
|
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
297 |
(* transform fact expressions *) |
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
298 |
|
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
299 |
fun transform_facts phi = map (fn ((a, atts), bs) => |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
300 |
((Morphism.binding phi a, (map o map) (Token.transform phi) atts), |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
301 |
bs |> map (fn (ths, btts) => (Morphism.fact phi ths, (map o map) (Token.transform phi) btts)))); |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
302 |
|
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58025
diff
changeset
|
303 |
|
5879 | 304 |
|
45586
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
305 |
(** partial evaluation -- observing rule/declaration/mixed attributes **) |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
306 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56052
diff
changeset
|
307 |
(*NB: result length may change due to rearrangement of symbolic expression*) |
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56052
diff
changeset
|
308 |
|
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
309 |
local |
45526 | 310 |
|
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
311 |
fun apply_att src (context, th) = |
45526 | 312 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
313 |
val src1 = map Token.init_assignable src; |
47815 | 314 |
val result = attribute_generic context src1 (context, th); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61527
diff
changeset
|
315 |
val src2 = map Token.closure src1; |
45526 | 316 |
in (src2, result) end; |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
317 |
|
45527
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
318 |
fun err msg src = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57942
diff
changeset
|
319 |
let val (name, pos) = Token.name_of_src src |
48992 | 320 |
in error (msg ^ " " ^ quote name ^ Position.here pos) end; |
45527
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
321 |
|
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
322 |
fun eval src ((th, dyn), (decls, context)) = |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
323 |
(case (apply_att src (context, th), dyn) of |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
324 |
((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context)) |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
325 |
| ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
326 |
| ((src', (SOME context', NONE)), NONE) => |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
327 |
let |
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
328 |
val decls' = |
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
329 |
(case decls of |
45526 | 330 |
[] => [(th, [src'])] |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
331 |
| (th2, srcs2) :: rest => |
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
52487
diff
changeset
|
332 |
if Thm.eq_thm_strict (th, th2) |
45526 | 333 |
then ((th2, src' :: srcs2) :: rest) |
334 |
else (th, [src']) :: (th2, srcs2) :: rest); |
|
45527
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
335 |
in ((th, NONE), (decls', context')) end |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
336 |
| ((src', (opt_context', opt_th')), _) => |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
337 |
let |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
338 |
val context' = the_default context opt_context'; |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
339 |
val th' = the_default th opt_th'; |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
340 |
val dyn' = |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
341 |
(case dyn of |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
342 |
NONE => SOME (th, [src']) |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
343 |
| SOME (dyn_th, srcs) => SOME (dyn_th, src' :: srcs)); |
d2b3d16b673a
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
wenzelm
parents:
45526
diff
changeset
|
344 |
in ((th', dyn'), (decls, context')) end); |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
345 |
|
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
346 |
in |
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
347 |
|
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
348 |
fun partial_evaluation ctxt facts = |
57858
39d9c7f175e0
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
wenzelm
parents:
56438
diff
changeset
|
349 |
(facts, Context.Proof (Context_Position.not_really ctxt)) |-> |
45586
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
350 |
fold_map (fn ((b, more_atts), fact) => fn context => |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
351 |
let |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
352 |
val (fact', (decls, context')) = |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
353 |
(fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 => |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
354 |
(ths, res1) |-> fold_map (fn th => fn res2 => |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
355 |
let |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
356 |
val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2); |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
357 |
val th_atts' = |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
358 |
(case dyn' of |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
359 |
NONE => (th', []) |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
360 |
| SOME (dyn_th', atts') => (dyn_th', rev atts')); |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
361 |
in (th_atts', res3) end)) |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
362 |
|>> flat; |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
363 |
val decls' = rev (map (apsnd rev) decls); |
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
364 |
val facts' = |
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
52487
diff
changeset
|
365 |
if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then |
45586
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
366 |
[((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')] |
45619 | 367 |
else if null decls' then [((b, []), fact')] |
63352 | 368 |
else [(Binding.empty_atts, decls'), ((b, []), fact')]; |
45586
c94f149cdf5d
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
wenzelm
parents:
45584
diff
changeset
|
369 |
in (facts', context') end) |
46906
3c1787d46935
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
wenzelm
parents:
46903
diff
changeset
|
370 |
|> fst |> flat |> map (apsnd (map (apfst single))) |
63352 | 371 |
|> filter_out (fn (b, fact) => Binding.is_empty_atts b andalso forall (null o #2) fact); |
45493
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
372 |
|
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
373 |
end; |
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
374 |
|
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
375 |
|
12453fd8dcff
some support for partial evaluation of attributed facts;
wenzelm
parents:
45491
diff
changeset
|
376 |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
377 |
(** configuration options **) |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
378 |
|
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
379 |
(* naming *) |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
380 |
|
33522 | 381 |
structure Configs = Theory_Data |
24713 | 382 |
( |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
383 |
type T = Config.raw Symtab.table; |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
384 |
val empty = Symtab.empty; |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
385 |
val extend = I; |
33522 | 386 |
fun merge data = Symtab.merge (K true) data; |
24713 | 387 |
); |
5823 | 388 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
389 |
fun print_options verbose ctxt = |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
390 |
let |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
391 |
fun prt (name, config) = |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
392 |
let val value = Config.get ctxt config in |
50301 | 393 |
Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="), |
394 |
Pretty.brk 1, Pretty.str (Config.print_value value)] |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
395 |
end; |
56027
25889f5c39a8
prefer Name_Space.pretty with its builtin markup;
wenzelm
parents:
56026
diff
changeset
|
396 |
val space = attribute_space ctxt; |
56052 | 397 |
val configs = |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59064
diff
changeset
|
398 |
Name_Space.markup_entries verbose ctxt space |
56052 | 399 |
(Symtab.dest (Configs.get (Proof_Context.theory_of ctxt))); |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
400 |
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
401 |
|
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
402 |
|
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
403 |
(* concrete syntax *) |
23988
aa46577f4f44
added attribute "option" for setting configuration options;
wenzelm
parents:
23937
diff
changeset
|
404 |
|
24003
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
405 |
local |
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
406 |
|
36950 | 407 |
val equals = Parse.$$$ "="; |
24003
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
408 |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
409 |
fun scan_value (Config.Bool _) = |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
410 |
equals -- Args.$$$ "false" >> K (Config.Bool false) || |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
411 |
equals -- Args.$$$ "true" >> K (Config.Bool true) || |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
412 |
Scan.succeed (Config.Bool true) |
36950 | 413 |
| scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int |
40291 | 414 |
| scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
415 |
| scan_value (Config.String _) = equals |-- Args.name >> Config.String; |
24003
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
416 |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
417 |
fun scan_config thy config = |
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36002
diff
changeset
|
418 |
let val config_type = Config.get_global thy config |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
419 |
in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end; |
24003
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
420 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
421 |
fun register binding config thy = |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
422 |
let val name = Sign.full_name thy binding in |
24126
913e1fa904fb
turned simp_depth_limit into configuration option;
wenzelm
parents:
24110
diff
changeset
|
423 |
thy |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
424 |
|> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option" |
24126
913e1fa904fb
turned simp_depth_limit into configuration option;
wenzelm
parents:
24110
diff
changeset
|
425 |
|> Configs.map (Symtab.update (name, config)) |
913e1fa904fb
turned simp_depth_limit into configuration option;
wenzelm
parents:
24110
diff
changeset
|
426 |
end; |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
427 |
|
42808
30870aee8a3f
discontinued global config options within attribute name space;
wenzelm
parents:
42669
diff
changeset
|
428 |
fun declare make coerce binding default = |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
429 |
let |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
430 |
val name = Binding.name_of binding; |
56438 | 431 |
val pos = Binding.pos_of binding; |
432 |
val config_value = Config.declare (name, pos) (make o default); |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
433 |
val config = coerce config_value; |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
434 |
in (config, register binding config_value) end; |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
435 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
436 |
in |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
437 |
|
56438 | 438 |
fun register_config config = |
439 |
register (Binding.make (Config.name_of config, Config.pos_of config)) config; |
|
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
440 |
|
42808
30870aee8a3f
discontinued global config options within attribute name space;
wenzelm
parents:
42669
diff
changeset
|
441 |
val config_bool = declare Config.Bool Config.bool; |
30870aee8a3f
discontinued global config options within attribute name space;
wenzelm
parents:
42669
diff
changeset
|
442 |
val config_int = declare Config.Int Config.int; |
30870aee8a3f
discontinued global config options within attribute name space;
wenzelm
parents:
42669
diff
changeset
|
443 |
val config_real = declare Config.Real Config.real; |
30870aee8a3f
discontinued global config options within attribute name space;
wenzelm
parents:
42669
diff
changeset
|
444 |
val config_string = declare Config.String Config.string; |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
445 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
446 |
end; |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
447 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
448 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
449 |
(* implicit setup *) |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
450 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
451 |
local |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24030
diff
changeset
|
452 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
453 |
fun setup_config declare_config binding default = |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
454 |
let |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
455 |
val (config, setup) = declare_config binding default; |
53171 | 456 |
val _ = Theory.setup setup; |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
457 |
in config end; |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
458 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
459 |
in |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
460 |
|
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
461 |
val setup_config_bool = setup_config config_bool; |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
462 |
val setup_config_int = setup_config config_int; |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
463 |
val setup_config_string = setup_config config_string; |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42380
diff
changeset
|
464 |
val setup_config_real = setup_config config_real; |
24003
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
465 |
|
da76d7e6435c
attribute "option": more elaborate syntax (with value parsing);
wenzelm
parents:
23988
diff
changeset
|
466 |
end; |
23988
aa46577f4f44
added attribute "option" for setting configuration options;
wenzelm
parents:
23937
diff
changeset
|
467 |
|
aa46577f4f44
added attribute "option" for setting configuration options;
wenzelm
parents:
23937
diff
changeset
|
468 |
|
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
469 |
(* system options *) |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
470 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
471 |
local |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
472 |
|
56438 | 473 |
fun declare_option coerce (name, pos) = |
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
474 |
let |
56438 | 475 |
val config = Config.declare_option (name, pos); |
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
476 |
in (coerce config, register_config config) end; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
477 |
|
56438 | 478 |
fun setup_option coerce (name, pos) = |
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
479 |
let |
56438 | 480 |
val config = Config.declare_option (name, pos); |
53171 | 481 |
val _ = Theory.setup (register_config config); |
52040
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
482 |
in coerce config end; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
483 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
484 |
in |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
485 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
486 |
val option_bool = declare_option Config.bool; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
487 |
val option_int = declare_option Config.int; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
488 |
val option_real = declare_option Config.real; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
489 |
val option_string = declare_option Config.string; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
490 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
491 |
val setup_option_bool = setup_option Config.bool; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
492 |
val setup_option_int = setup_option Config.int; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
493 |
val setup_option_real = setup_option Config.real; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
494 |
val setup_option_string = setup_option Config.string; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
495 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
496 |
end; |
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
497 |
|
852939d19216
system options as context-sensitive configuration options within the attribute name space;
wenzelm
parents:
52039
diff
changeset
|
498 |
|
18636 | 499 |
(* theory setup *) |
5823 | 500 |
|
53171 | 501 |
val _ = Theory.setup |
67147 | 502 |
(setup \<^binding>\<open>tagged\<close> (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #> |
503 |
setup \<^binding>\<open>untagged\<close> (Scan.lift Args.name >> Thm.untag) "untagged theorem" #> |
|
504 |
setup \<^binding>\<open>kind\<close> (Scan.lift Args.name >> Thm.kind) "theorem kind" #> |
|
505 |
setup \<^binding>\<open>THEN\<close> |
|
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
506 |
(Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
507 |
>> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
508 |
"resolution with rule" #> |
67147 | 509 |
setup \<^binding>\<open>OF\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
510 |
(thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
511 |
"rule resolved with facts" #> |
67147 | 512 |
setup \<^binding>\<open>rename_abs\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
513 |
(Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
514 |
Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
515 |
"rename bound variables in abstractions" #> |
67147 | 516 |
setup \<^binding>\<open>unfolded\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
517 |
(thms >> (fn ths => |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
518 |
Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
519 |
"unfolded definitions" #> |
67147 | 520 |
setup \<^binding>\<open>folded\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
521 |
(thms >> (fn ths => |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
522 |
Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
523 |
"folded definitions" #> |
67147 | 524 |
setup \<^binding>\<open>consumes\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
525 |
(Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
526 |
"number of consumed facts" #> |
67147 | 527 |
setup \<^binding>\<open>constraints\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
528 |
(Scan.lift Parse.nat >> Rule_Cases.constraints) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
529 |
"number of equality constraints" #> |
67147 | 530 |
setup \<^binding>\<open>cases_open\<close> |
63019 | 531 |
(Scan.succeed Rule_Cases.cases_open) |
532 |
"rule with open parameters" #> |
|
67147 | 533 |
setup \<^binding>\<open>case_names\<close> |
63019 | 534 |
(Scan.lift (Scan.repeat (Args.name -- |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
535 |
Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [])) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
536 |
>> (fn cs => |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
537 |
Rule_Cases.cases_hyp_names |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
538 |
(map #1 cs) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
539 |
(map (map (the_default Rule_Cases.case_hypsN) o #2) cs))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
540 |
"named rule cases" #> |
67147 | 541 |
setup \<^binding>\<open>case_conclusion\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
542 |
(Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
543 |
"named conclusion of rule cases" #> |
67147 | 544 |
setup \<^binding>\<open>params\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
545 |
(Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
546 |
"named rule parameters" #> |
67147 | 547 |
setup \<^binding>\<open>rule_format\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
548 |
(Scan.lift (Args.mode "no_asm") |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
549 |
>> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
550 |
"result put into canonical rule format" #> |
67147 | 551 |
setup \<^binding>\<open>elim_format\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
552 |
(Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
553 |
"destruct rule turned into elimination rule format" #> |
67147 | 554 |
setup \<^binding>\<open>no_vars\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
555 |
(Scan.succeed (Thm.rule_attribute [] (fn context => fn th => |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
556 |
let |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
557 |
val ctxt = Variable.set_body false (Context.proof_of context); |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
558 |
val ((_, [th']), _) = Variable.import true [th] ctxt; |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
559 |
in th' end))) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
560 |
"imported schematic variables" #> |
67147 | 561 |
setup \<^binding>\<open>atomize\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
562 |
(Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #> |
67147 | 563 |
setup \<^binding>\<open>rulify\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
564 |
(Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #> |
67147 | 565 |
setup \<^binding>\<open>rotated\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
566 |
(Scan.lift (Scan.optional Parse.int 1 |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
567 |
>> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #> |
67147 | 568 |
setup \<^binding>\<open>defn\<close> |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
569 |
(add_del Local_Defs.defn_add Local_Defs.defn_del) |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
570 |
"declaration of definitional transformations" #> |
67147 | 571 |
setup \<^binding>\<open>abs_def\<close> |
63068
8b9401bfd9fd
unfold is subject to unfold_abs_def (still inactive);
wenzelm
parents:
63019
diff
changeset
|
572 |
(Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of))) |
62898
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
573 |
"abstract over free variables of definitional theorem" #> |
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
574 |
|
fdc290b68ecd
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
wenzelm
parents:
62878
diff
changeset
|
575 |
register_config Goal.quick_and_dirty_raw #> |
52059 | 576 |
register_config Ast.trace_raw #> |
43347 | 577 |
register_config Ast.stats_raw #> |
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
578 |
register_config Printer.show_brackets_raw #> |
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
579 |
register_config Printer.show_sorts_raw #> |
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
580 |
register_config Printer.show_types_raw #> |
49657
40e4feac2921
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
wenzelm
parents:
48992
diff
changeset
|
581 |
register_config Printer.show_markup_raw #> |
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
582 |
register_config Printer.show_structs_raw #> |
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
583 |
register_config Printer.show_question_marks_raw #> |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
584 |
register_config Syntax.ambiguity_warning_raw #> |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46126
diff
changeset
|
585 |
register_config Syntax.ambiguity_limit_raw #> |
42284 | 586 |
register_config Syntax_Trans.eta_contract_raw #> |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42616
diff
changeset
|
587 |
register_config Name_Space.names_long_raw #> |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42616
diff
changeset
|
588 |
register_config Name_Space.names_short_raw #> |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42616
diff
changeset
|
589 |
register_config Name_Space.names_unique_raw #> |
62878 | 590 |
register_config ML_Print_Depth.print_depth_raw #> |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68558
diff
changeset
|
591 |
register_config ML_Env.ML_environment_raw #> |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68558
diff
changeset
|
592 |
register_config ML_Env.ML_read_global_raw #> |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68558
diff
changeset
|
593 |
register_config ML_Env.ML_write_global_raw #> |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
594 |
register_config ML_Options.source_trace_raw #> |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56281
diff
changeset
|
595 |
register_config ML_Options.exception_trace_raw #> |
62498 | 596 |
register_config ML_Options.exception_debugger_raw #> |
60743 | 597 |
register_config ML_Options.debugger_raw #> |
42360 | 598 |
register_config Proof_Context.show_abbrevs_raw #> |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
599 |
register_config Goal_Display.goals_limit_raw #> |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
600 |
register_config Goal_Display.show_main_goal_raw #> |
61268 | 601 |
register_config Thm.show_consts_raw #> |
602 |
register_config Thm.show_hyps_raw #> |
|
603 |
register_config Thm.show_tags_raw #> |
|
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52683
diff
changeset
|
604 |
register_config Pattern.unify_trace_failure_raw #> |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
605 |
register_config Unify.trace_bound_raw #> |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
606 |
register_config Unify.search_bound_raw #> |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
607 |
register_config Unify.trace_simp_raw #> |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39137
diff
changeset
|
608 |
register_config Unify.trace_types_raw #> |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41183
diff
changeset
|
609 |
register_config Raw_Simplifier.simp_depth_limit_raw #> |
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41183
diff
changeset
|
610 |
register_config Raw_Simplifier.simp_trace_depth_limit_raw #> |
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41183
diff
changeset
|
611 |
register_config Raw_Simplifier.simp_debug_raw #> |
63068
8b9401bfd9fd
unfold is subject to unfold_abs_def (still inactive);
wenzelm
parents:
63019
diff
changeset
|
612 |
register_config Raw_Simplifier.simp_trace_raw #> |
8b9401bfd9fd
unfold is subject to unfold_abs_def (still inactive);
wenzelm
parents:
63019
diff
changeset
|
613 |
register_config Local_Defs.unfold_abs_def_raw); |
5823 | 614 |
|
63019 | 615 |
|
616 |
(* internal source *) |
|
617 |
||
618 |
local |
|
619 |
||
620 |
val internal = internal_name (Context.the_local_context ()); |
|
621 |
||
622 |
val consumes_name = internal "consumes"; |
|
623 |
val constraints_name = internal "constraints"; |
|
624 |
val cases_open_name = internal "cases_open"; |
|
625 |
val case_names_name = internal "case_names"; |
|
626 |
val case_conclusion_name = internal "case_conclusion"; |
|
627 |
||
628 |
fun make_string s = Token.make_string (s, Position.none); |
|
629 |
||
630 |
in |
|
631 |
||
632 |
fun consumes i = consumes_name :: Token.make_int i; |
|
633 |
fun constraints i = constraints_name :: Token.make_int i; |
|
634 |
val cases_open = [cases_open_name]; |
|
635 |
fun case_names names = case_names_name :: map make_string names; |
|
636 |
fun case_conclusion (name, names) = case_conclusion_name :: map make_string (name :: names); |
|
637 |
||
5823 | 638 |
end; |
63019 | 639 |
|
640 |
end; |