tuned signature;
authorwenzelm
Fri, 30 Dec 2022 13:25:29 +0100
changeset 76826 eb3b946bdeff
parent 76825 65e8a9272837
child 76827 a150dd0ebdd3
tuned signature;
src/Pure/Thy/document_build.scala
src/Pure/Thy/latex.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(
--- 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)