--- a/NEWS Sat Feb 04 20:12:27 2017 +0100
+++ b/NEWS Sat Feb 04 21:15:11 2017 +0100
@@ -7,6 +7,12 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Document antiquotations @{prf} and @{full_prf} output proof terms
+(again) in the same way as commands 'prf' and 'full_prf'.
+
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Sat Feb 04 20:12:27 2017 +0100
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Sat Feb 04 21:15:11 2017 +0100
@@ -20,12 +20,17 @@
qed
ML_val \<open>
+ val thm = @{thm ex};
+
(*proof body with digest*)
- val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
+ val body = Proofterm.strip_thm (Thm.proof_body_of thm);
(*proof term only*)
val prf = Proofterm.proof_of body;
- Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
+
+ (*clean output*)
+ Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} false thm);
+ Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} true thm);
(*all theorems used in the graph of nested proofs*)
val all_thms =
--- a/src/HOL/Proofs/ex/XML_Data.thy Sat Feb 04 20:12:27 2017 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy Sat Feb 04 21:15:11 2017 +0100
@@ -6,25 +6,14 @@
*)
theory XML_Data
-imports "~~/src/HOL/Isar_Examples/Drinker"
+ imports "~~/src/HOL/Isar_Examples/Drinker"
begin
subsection \<open>Export and re-import of global proof terms\<close>
ML \<open>
fun export_proof ctxt thm =
- let
- val thy = Proof_Context.theory_of ctxt;
- val (_, prop) =
- Logic.unconstrainT (Thm.shyps_of thm)
- (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
- val prf =
- Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
- Reconstruct.reconstruct_proof ctxt prop |>
- Reconstruct.expand_proof ctxt [("", NONE)] |>
- Proofterm.rew_proof thy |>
- Proofterm.no_thm_proofs;
- in Proofterm.encode prf end;
+ Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm);
fun import_proof thy xml =
let
--- a/src/Pure/Isar/isar_cmd.ML Sat Feb 04 20:12:27 2017 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Feb 04 21:15:11 2017 +0100
@@ -260,21 +260,7 @@
| SOME srcs =>
let
val ctxt = Toplevel.context_of state;
- val thy = Proof_Context.theory_of ctxt;
- fun pretty_proof thm =
- let
- val (_, prop) =
- Logic.unconstrainT (Thm.shyps_of thm)
- (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
- in
- Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
- |> Reconstruct.reconstruct_proof ctxt prop
- |> Reconstruct.expand_proof ctxt [("", NONE)]
- |> Proofterm.rew_proof thy
- |> Proofterm.no_thm_proofs
- |> not full ? Proofterm.shrink_proof
- |> Proof_Syntax.pretty_proof ctxt
- end;
+ val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
fun string_of_prop ctxt s =
--- a/src/Pure/Proof/proof_syntax.ML Sat Feb 04 20:12:27 2017 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Sat Feb 04 21:15:11 2017 +0100
@@ -16,7 +16,7 @@
val proof_syntax: Proofterm.proof -> theory -> theory
val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
- val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
+ val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
structure Proof_Syntax : PROOF_SYNTAX =
@@ -259,7 +259,7 @@
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
(term_of_proof prf);
-fun pretty_proof_of ctxt full th =
- pretty_proof ctxt (proof_of ctxt full th);
+fun pretty_clean_proof_of ctxt full thm =
+ pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);
end;
--- a/src/Pure/Proof/reconstruct.ML Sat Feb 04 20:12:27 2017 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sat Feb 04 21:15:11 2017 +0100
@@ -13,6 +13,7 @@
val proof_of : Proof.context -> thm -> Proofterm.proof
val expand_proof : Proof.context -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
+ val clean_proof_of : Proof.context -> bool -> thm -> Proofterm.proof
end;
structure Reconstruct : RECONSTRUCT =
@@ -388,4 +389,21 @@
in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
+
+(* cleanup for output etc. *)
+
+fun clean_proof_of ctxt full thm =
+ let
+ val (_, prop) =
+ Logic.unconstrainT (Thm.shyps_of thm)
+ (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
+ in
+ Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
+ |> reconstruct_proof ctxt prop
+ |> expand_proof ctxt [("", NONE)]
+ |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
+ |> Proofterm.no_thm_proofs
+ |> not full ? Proofterm.shrink_proof
+ end;
+
end;
--- a/src/Pure/Thy/thy_output.ML Sat Feb 04 20:12:27 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Feb 04 21:15:11 2017 +0100
@@ -584,7 +584,7 @@
let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
in Pretty.str (Proof_Context.extern_type ctxt name) end;
-fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);