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