# HG changeset patch
# User wenzelm
# Date 1572894623 -3600
# Node ID 35a8e15b7e036b45edb6296b8ccf7fe9629eafc7
# Parent  6504ea98623c55f3453304aa82e96cfab845381c
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;

diff -r 6504ea98623c -r 35a8e15b7e03 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 04 16:56:16 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 04 20:10:23 2019 +0100
@@ -294,7 +294,9 @@
       let
         val State ((node', pr_ctxt), _) =
           node |> apply
-            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
+            (fn _ =>
+              node_presentation
+                (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
             (K ());
       in State ((Toplevel, pr_ctxt), get_theory node') end
   | (Keep f, node) =>
diff -r 6504ea98623c -r 35a8e15b7e03 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Nov 04 16:56:16 2019 +0100
+++ b/src/Pure/more_thm.ML	Mon Nov 04 20:10:23 2019 +0100
@@ -118,6 +118,7 @@
     thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
+  val expose_theory: theory -> unit
   val show_consts: bool Config.T
   val show_hyps: bool Config.T
   val show_tags: bool Config.T
@@ -681,14 +682,13 @@
 fun register_proofs ths =
   (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
 
-fun consolidate_theory thy =
-  let
-    val thms =
-      rev (Proofs.get thy)
-      |> maps (map (Thm.transfer thy) o Lazy.force);
-    val _ = Thm.consolidate thms;
-    val _ = Thm.expose_proofs thy thms;
-  in () end;
+fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force);
+
+val consolidate_theory = Thm.consolidate o force_proofs;
+
+fun expose_theory thy =
+  if Proofterm.export_enabled ()
+  then Thm.expose_proofs thy (force_proofs thy) else ();