Commands prf and full_prf can now also be used to display proof term
of current proof state.
--- a/src/Pure/Isar/isar_cmd.ML Fri Nov 09 00:20:26 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Fri Nov 09 10:25:10 2001 +0100
@@ -60,7 +60,7 @@
val print_cases: Toplevel.transition -> Toplevel.transition
val print_thms: (string list * (string * Args.src list) list) * Comment.text
-> Toplevel.transition -> Toplevel.transition
- val print_prfs: bool -> (string list * (string * Args.src list) list) * Comment.text
+ val print_prfs: bool -> (string list * (string * Args.src list) list option) * Comment.text
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) * Comment.text
-> Toplevel.transition -> Toplevel.transition
@@ -240,9 +240,19 @@
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
(IsarThy.get_thmss args state)));
-fun string_of_prfs full state ms args = with_modes ms (fn () =>
- Pretty.string_of (Pretty.chunks (* FIXME context syntax!? *)
- (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
+fun string_of_prfs full state ms arg = with_modes ms (fn () =>
+ Pretty.string_of (case arg of (* FIXME context syntax!? *)
+ None =>
+ let
+ val (_, (_, thm)) = Proof.get_goal state;
+ val {sign, prop, der = (_, prf), ...} = rep_thm thm;
+ val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
+ in
+ ProofSyntax.pretty_proof sign
+ (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
+ end
+ | Some args => Pretty.chunks
+ (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
fun string_of_prop state ms s =
let
--- a/src/Pure/Isar/isar_syn.ML Fri Nov 09 00:20:26 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Nov 09 10:25:10 2001 +0100
@@ -613,11 +613,13 @@
val print_prfsP =
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
- (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
+ (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
+ (Toplevel.no_timing oo IsarCmd.print_prfs false));
val print_full_prfsP =
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
- (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
+ (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >>
+ (Toplevel.no_timing oo IsarCmd.print_prfs true));
val print_propP =
OuterSyntax.improper_command "prop" "read and print proposition" K.diag