# HG changeset patch
# User wenzelm
# Date 1621978652 -7200
# Node ID b5fb99b985b4525f4587a19fe792ce97783a2b82
# Parent  04d39959d1e64ebc036a218e655f4afe2aa2780f
clarified document export names;

diff -r 04d39959d1e6 -r b5fb99b985b4 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue May 25 23:18:29 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue May 25 23:37:32 2021 +0200
@@ -218,7 +218,7 @@
       for (name <- document_theories)
       yield {
         val path = Path.basic(tex_name(name))
-        val xml = YXML.parse_body(get_export(name.theory, document_tex_name(name)).text)
+        val xml = YXML.parse_body(get_export(name.theory, Export.DOCUMENT_LATEX).text)
         val content = Latex.output(xml, file_pos = name.path.implode_symbolic)
         Content(path, content)
       }
@@ -426,7 +426,6 @@
   /* build documents */
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
-  def document_tex_name(name: Document.Node.Name): String = Export.DOCUMENT_PREFIX + tex_name(name)
 
   class Build_Error(val log_lines: List[String], val message: String)
     extends Exn.User_Error(message)
diff -r 04d39959d1e6 -r b5fb99b985b4 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue May 25 23:18:29 2021 +0200
+++ b/src/Pure/Thy/export.scala	Tue May 25 23:37:32 2021 +0200
@@ -20,7 +20,8 @@
   val MARKUP = "PIDE/markup"
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
-  val CITATIONS = DOCUMENT_PREFIX + "citations"
+  val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
+  val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"
 
diff -r 04d39959d1e6 -r b5fb99b985b4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue May 25 23:18:29 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue May 25 23:37:32 2021 +0200
@@ -30,14 +30,6 @@
 
 (** theory presentation **)
 
-(* artefact names *)
-
-fun document_name ext thy =
-  Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
-
-val document_tex_name = document_name "tex";
-
-
 (* hook for consolidated theory *)
 
 type presentation_context =
@@ -77,9 +69,8 @@
         else
           let
             val thy_name = Context.theory_name thy;
-            val document_tex_name = document_tex_name thy;
             val latex = Latex.isabelle_body thy_name body;
-          in Export.export thy document_tex_name latex end
+          in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end
       end));
 
 
diff -r 04d39959d1e6 -r b5fb99b985b4 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue May 25 23:18:29 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue May 25 23:37:32 2021 +0200
@@ -384,7 +384,7 @@
             export(Export.MESSAGES, snapshot.messages.map(_._1))
 
             val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
-            export_text(Export.CITATIONS, cat_lines(citations))
+            export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations))
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")