# HG changeset patch
# User wenzelm
# Date 1606322949 -3600
# Node ID 6bc199a70bf9cea783fe32b221e6692200e7f8bd
# Parent  cb9d5af781b480744e85f6a0d9fd7eda30c6e813
more robust: include reports from Thy_Output.present_thy/output_document;

diff -r cb9d5af781b4 -r 6bc199a70bf9 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Nov 25 16:14:16 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Nov 25 17:49:09 2020 +0100
@@ -56,13 +56,13 @@
 );
 
 fun apply_presentation (context: presentation_context) thy =
-  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+ (ignore (Par_List.map (fn (f, _) => f context thy (Presentation.get thy)));
+  Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []);
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
-   (Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) [];
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
@@ -77,7 +77,7 @@
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
           in Export.export thy document_tex_name (XML.blob output) end
-      end)));
+      end));