71 |
71 |
72 val introN = "intro"; |
72 val introN = "intro"; |
73 val elimN = "elim"; |
73 val elimN = "elim"; |
74 val destN = "dest"; |
74 val destN = "dest"; |
75 |
75 |
76 fun modifier name kind kind' att = |
76 fun modifier name kind kind' att pos = |
77 Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME) |
77 Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME) |
78 >> (pair (I: Proof.context -> Proof.context) o att); |
78 >> (fn arg => Method.modifier (att arg) pos); |
79 |
79 |
80 val modifiers = |
80 val modifiers = |
81 [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang, |
81 [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here}, |
82 modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest, |
82 modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here}, |
83 modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang, |
83 modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here}, |
84 modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim, |
84 modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here}, |
85 modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang, |
85 modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here}, |
86 modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro, |
86 modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here}, |
87 Args.del -- Args.colon >> K (I, Context_Rules.rule_del)]; |
87 Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})]; |
88 |
88 |
89 in |
89 in |
90 |
90 |
91 fun method_setup name = |
91 fun method_setup name = |
92 Method.setup name |
92 Method.setup name |