--- 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)