equal
deleted
inserted
replaced
453 |
453 |
454 |
454 |
455 |
455 |
456 (** command syntax **) |
456 (** command syntax **) |
457 |
457 |
458 fun find_theorems_cmd ((opt_lim, rem_dups), spec) = |
|
459 Toplevel.unknown_theory o Toplevel.keep (fn state => |
|
460 let |
|
461 val proof_state = Toplevel.enter_proof_body state; |
|
462 val ctxt = Proof.context_of proof_state; |
|
463 val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal; |
|
464 in print_theorems ctxt opt_goal opt_lim rem_dups spec end); |
|
465 |
|
466 local |
458 local |
467 |
459 |
468 val criterion = |
460 val criterion = |
469 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
461 Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
470 Parse.reserved "intro" >> K Intro || |
462 Parse.reserved "intro" >> K Intro || |
484 |
476 |
485 val _ = |
477 val _ = |
486 Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" |
478 Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" |
487 Keyword.diag |
479 Keyword.diag |
488 (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)) |
480 (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)) |
489 >> (Toplevel.no_timing oo find_theorems_cmd)); |
481 >> (fn ((opt_lim, rem_dups), spec) => |
|
482 Toplevel.no_timing o |
|
483 Toplevel.keep (fn state => |
|
484 let |
|
485 val ctxt = Toplevel.context_of state; |
|
486 val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; |
|
487 in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); |
490 |
488 |
491 end; |
489 end; |
492 |
490 |
493 end; |
491 end; |