# HG changeset patch
# User wenzelm
# Date 1667576139 -3600
# Node ID d0079b509d996e2fabd46dff9a0c5b7080c6ac32
# Parent  773844f3273d433ffbfc49dfb4500d8f1b7d87d3
clarified signature;

diff -r 773844f3273d -r d0079b509d99 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Fri Nov 04 15:34:23 2022 +0100
+++ b/src/Pure/Thy/document_output.ML	Fri Nov 04 16:35:39 2022 +0100
@@ -16,7 +16,7 @@
   type segment =
     {span: Command_Span.span, command: Toplevel.transition,
      prev_state: Toplevel.state, state: Toplevel.state}
-  val present_thy: Options.T -> Keyword.keywords -> segment list -> Latex.text
+  val present_thy: Options.T -> Keyword.keywords -> string -> segment list -> Latex.text
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val isabelle: Proof.context -> Latex.text -> Latex.text
@@ -400,7 +400,7 @@
 
 in
 
-fun present_thy options keywords (segments: segment list) =
+fun present_thy options keywords thy_name (segments: segment list) =
   let
     (* tokens *)
 
@@ -479,6 +479,7 @@
       |> present (Toplevel.make_state NONE) (spans ~~ command_results)
       |> present_trailer
       |> rev
+      |> Latex.isabelle_body thy_name
     else error "Messed-up outer syntax for presentation"
   end;
 
diff -r 773844f3273d -r d0079b509d99 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Nov 04 15:34:23 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Nov 04 16:35:39 2022 +0100
@@ -59,14 +59,12 @@
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
-        val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments;
+        val keywords = Thy_Header.get_keywords thy;
+        val thy_name = Context.theory_name thy;
+        val latex = Document_Output.present_thy options keywords thy_name segments;
       in
         if Options.string options "document" = "false" then ()
-        else
-          let
-            val thy_name = Context.theory_name thy;
-            val latex = Latex.isabelle_body thy_name body;
-          in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end
+        else Export.export thy \<^path_binding>\<open>document/latex\<close> latex
       end));