equal
deleted
inserted
replaced
280 val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout)); |
280 val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout)); |
281 val _ = kill (); (*RACE wrt. other invocations of sledgehammer*) |
281 val _ = kill (); (*RACE wrt. other invocations of sledgehammer*) |
282 val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers; |
282 val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers; |
283 in () end; |
283 in () end; |
284 |
284 |
285 |
|
286 |
|
287 (** Isar command syntax **) |
|
288 |
|
289 local structure K = OuterKeyword and P = OuterParse in |
|
290 |
|
291 val _ = |
|
292 OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag |
|
293 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); |
|
294 |
|
295 val _ = |
|
296 OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag |
|
297 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)); |
|
298 |
|
299 val _ = |
|
300 OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag |
|
301 (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> |
|
302 (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit))); |
|
303 |
|
304 val _ = |
|
305 OuterSyntax.improper_command "print_atps" "print external provers" K.diag |
|
306 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o |
|
307 Toplevel.keep (print_provers o Toplevel.theory_of))); |
|
308 |
|
309 val _ = |
|
310 OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag |
|
311 (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o |
|
312 Toplevel.keep (sledgehammer names o Toplevel.proof_of))); |
|
313 |
|
314 end; |
285 end; |
315 |
|
316 end; |
|
317 |
|