# HG changeset patch # User wenzelm # Date 1572628126 -3600 # Node ID 5e98925f86ede3a9bc68bf0d74a4b9455623c5b0 # Parent 52a62342c9ce85e4f48ffe615c6516e214380464 clarified signature (again); diff -r 52a62342c9ce -r 5e98925f86ed src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Fri Nov 01 17:53:27 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Fri Nov 01 18:08:46 2019 +0100 @@ -289,7 +289,9 @@ else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); - val _ = Proofterm.commit_proof thy proof; + val _ = + if Proofterm.export_proof_boxes_required thy + then Proofterm.export_proof_boxes [proof] else (); in (prop, (deps, (boxes, proof))) |> let diff -r 52a62342c9ce -r 5e98925f86ed src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Nov 01 17:53:27 2019 +0100 +++ b/src/Pure/proofterm.ML Fri Nov 01 18:08:46 2019 +0100 @@ -174,8 +174,9 @@ val export_enabled: unit -> bool val export_standard_enabled: unit -> bool + val export_proof_boxes_required: theory -> bool + val export_proof_boxes: proof list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body - val commit_proof: theory -> proof -> unit val thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> string * Position.T -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof @@ -2091,7 +2092,11 @@ fun export_enabled () = Options.default_bool "export_proofs"; fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; -fun export_proof_boxes proof = +fun export_proof_boxes_required thy = + Context.theory_name thy = Context.PureN orelse + (export_enabled () andalso not (export_standard_enabled ())); + +fun export_proof_boxes proofs = let fun export_boxes (AbsP (_, _, prf)) = export_boxes prf | export_boxes (Abst (_, _, prf)) = export_boxes prf @@ -2107,14 +2112,9 @@ val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export); in export_boxes prf' boxes' end) | export_boxes _ = I; - val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest; + val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest; in List.app (Lazy.force o #2) boxes end; -fun commit_proof thy proof = - if Context.theory_name thy = Context.PureN orelse - (export_enabled () andalso not (export_standard_enabled ())) - then export_proof_boxes proof else (); - local fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) = @@ -2163,7 +2163,7 @@ fun export thy i prop prf = if export_enabled () then let - val _ = export_proof_boxes prf; + val _ = export_proof_boxes [prf]; val _ = export_proof thy i prop prf; in () end else ();