# HG changeset patch
# User berghofe
# Date 1005297910 -3600
# Node ID 316d11f760f7469c3e67624a38a528626c366fb7
# Parent  c4fcdb80c93e29813f9c0600c074203ad766a541
Commands prf and full_prf can now also be used to display proof term
of current proof state.

diff -r c4fcdb80c93e -r 316d11f760f7 src/Pure/Isar/isar_cmd.ML
--- 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
diff -r c4fcdb80c93e -r 316d11f760f7 src/Pure/Isar/isar_syn.ML
--- 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