# HG changeset patch
# User wenzelm
# Date 1601128974 -7200
# Node ID 9a7a1411796797b680e0010349b6cc1e06196fa1
# Parent  a756e464e9e3eed44bca74d4fb76d4c5c1e5f22d
clarified document export;

diff -r a756e464e9e3 -r 9a7a14117967 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Sep 26 16:02:41 2020 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Sep 26 16:02:54 2020 +0200
@@ -66,9 +66,12 @@
         if #disabled option then ()
         else
           let
-            val latex = Latex.isabelle_body (Context.theory_name thy) body;
+            val thy_name = Context.theory_name thy;
+            val document_path = Path.append (Path.basic "document") (Present.tex_path thy_name);
+
+            val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
-            val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
+            val _ = Export.export thy (Path.binding0 document_path) (XML.blob output);
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));