equal
deleted
inserted
replaced
142 end; |
142 end; |
143 |
143 |
144 |
144 |
145 (* command syntax *) |
145 (* command syntax *) |
146 |
146 |
147 fun find_consts_cmd spec = |
147 local |
148 Toplevel.unknown_theory o Toplevel.keep (fn state => |
|
149 find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec); |
|
150 |
148 |
151 val criterion = |
149 val criterion = |
152 Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict || |
150 Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict || |
153 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
151 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
154 Parse.xname >> Loose; |
152 Parse.xname >> Loose; |
155 |
153 |
|
154 in |
|
155 |
156 val _ = |
156 val _ = |
157 Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag |
157 Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag |
158 (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion) |
158 (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion) |
159 >> (Toplevel.no_timing oo find_consts_cmd)); |
159 >> (fn spec => Toplevel.no_timing o |
|
160 Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec))); |
160 |
161 |
161 end; |
162 end; |
162 |
163 |
|
164 end; |
|
165 |