# HG changeset patch
# User wenzelm
# Date 1667381084 -3600
# Node ID 4de3d831ff4d00fb05913d05dcc92ecac6c1a369
# Parent  fb9c567a67cd0d9a949a5c27c1112894c9fc4f96
clarified signature: do not require finished theory;

diff -r fb9c567a67cd -r 4de3d831ff4d src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Wed Nov 02 09:47:27 2022 +0100
+++ b/src/Pure/Thy/document_output.ML	Wed Nov 02 10:24:44 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 -> theory -> segment list -> Latex.text
+  val present_thy: Options.T -> Keyword.keywords -> 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
@@ -401,11 +401,8 @@
 
 in
 
-fun present_thy options thy (segments: segment list) =
+fun present_thy options keywords (segments: segment list) =
   let
-    val keywords = Thy_Header.get_keywords thy;
-
-
     (* tokens *)
 
     val ignored = Scan.state --| ignore
diff -r fb9c567a67cd -r 4de3d831ff4d src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Nov 02 09:47:27 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Nov 02 10:24:44 2022 +0100
@@ -58,7 +58,7 @@
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
-        val body = Document_Output.present_thy options thy segments;
+        val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments;
       in
         if Options.string options "document" = "false" then ()
         else