# HG changeset patch
# User wenzelm
# Date 1563804940 -7200
# Node ID 425c5f9bc61a01e51df106e3b9003f9150d7131f
# Parent  af88c05696bdf5cafc9d7e569dae1744088fd482
support export_proofs, prune_proofs;
tuned comments;

diff -r af88c05696bd -r 425c5f9bc61a etc/options
--- a/etc/options	Mon Jul 22 14:47:21 2019 +0200
+++ b/etc/options	Mon Jul 22 16:15:40 2019 +0200
@@ -277,8 +277,16 @@
 section "Theory Export"
 
 option export_document : bool = false
+  -- "export document sources to Isabelle/Scala"
 
 option export_theory : bool = false
+  -- "export theory content to Isabelle/Scala"
+
+option export_proofs : bool = false
+  -- "export proof terms to Isabelle/Scala"
+
+option prune_proofs : bool = false
+  -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
diff -r af88c05696bd -r 425c5f9bc61a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 22 14:47:21 2019 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 22 16:15:40 2019 +0200
@@ -129,6 +129,7 @@
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
+ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
@@ -305,7 +306,6 @@
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
-ML_file "Thy/export.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "Thy/export_theory.ML";
diff -r af88c05696bd -r 425c5f9bc61a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 14:47:21 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 22 16:15:40 2019 +0200
@@ -36,6 +36,7 @@
   type pthm = serial * thm_node
   type oracle = string * term
   val proof_of: proof_body -> proof
+  val map_proof_of: (proof -> proof) -> proof_body -> proof_body
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
@@ -190,6 +191,9 @@
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
+fun map_proof_of f (PBody {oracles, thms, proof}) =
+  PBody {oracles = oracles, thms = thms, proof = f proof};
+
 fun rep_thm_node (Thm_Node args) = args;
 val thm_node_name = #name o rep_thm_node;
 val thm_node_prop = #prop o rep_thm_node;
@@ -1307,9 +1311,6 @@
       | needed _ _ _ = [];
   in fn prf => #4 (shrink [] 0 prf) end;
 
-fun shrink_proof_body (PBody {oracles, thms, proof}) =
-  PBody {oracles = oracles, thms = thms, proof = shrink_proof proof};
-
 
 (**** Simple first order matching functions for terms and proofs ****)
 
@@ -1671,19 +1672,29 @@
       else
         let
           val rew = rew_proof thy;
-          val prf' = fold_rev implies_intr_proof hyps prf;
+          val prf0 = fold_rev implies_intr_proof hyps prf;
         in
           (singleton o Future.cond_forks)
             {name = "Proofterm.prepare_thm_proof", group = NONE,
               deps = [], pri = 1, interrupts = true}
-            (fn () => make_body0 (rew prf'))
+            (fn () => make_body0 (rew prf0))
         end;
 
-    val postproc =
-      unconstrainT_body thy (atyp_map, constraints) #> shrink_proof_body;
+    fun new_prf () =
+      let
+        val i = serial ();
+        fun export prf1 =
+         (if Options.default_bool "export_proofs" then
+            Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
+              (Buffer.chunks
+                (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
+          else ();
+          if Options.default_bool "prune_proofs" then MinProof else prf1);
+        val postproc =
+          unconstrainT_body thy (atyp_map, constraints) #>
+          map_proof_of (export #> shrink_proof);
+      in (i, fulfill_proof_future thy promises postproc body0) end;
 
-    fun new_prf () =
-      (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of