# HG changeset patch
# User wenzelm
# Date 1672403129 -3600
# Node ID eb3b946bdeffc710521242ba322cc7acd165578d
# Parent  65e8a9272837157018d13a25fb092bab2ae5e0f2
tuned signature;

diff -r 65e8a9272837 -r eb3b946bdeff src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Dec 30 12:41:08 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Dec 30 13:25:29 2022 +0100
@@ -140,7 +140,7 @@
     def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
     def file_pos: String = name.path.implode_symbolic
     def write(latex_output: Latex.Output, dir: Path): Unit =
-      content.output(latex_output(_, file_pos = file_pos)).write(dir)
+      content.output(latex_output.make(_, file_pos = file_pos)).write(dir)
   }
 
   def context(
diff -r 65e8a9272837 -r eb3b946bdeff src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Fri Dec 30 12:41:08 2022 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Dec 30 13:25:29 2022 +0100
@@ -158,7 +158,7 @@
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
   class Output(val options: Options) {
-    def latex_output(latex_text: Text): String = apply(latex_text)
+    def latex_output(latex_text: Text): String = make(latex_text)
 
     def latex_macro0(name: String, optional_argument: String = ""): Text =
       XML.string("\\" + name + optional_argument)
@@ -214,7 +214,7 @@
       error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
         ":\n" + XML.string_of_tree(elem))
 
-    def apply(latex_text: Text, file_pos: String = ""): String = {
+    def make(latex_text: Text, file_pos: String = ""): String = {
       var line = 1
       val result = new mutable.ListBuffer[String]
       val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)