# HG changeset patch
# User wenzelm
# Date 1621976669 -7200
# Node ID 4606a9cadd83fe5af3804ef9e93af09824593446
# Parent  0909fd14f8a40fbe810ec110293f92656f8d1193
tuned;

diff -r 0909fd14f8a4 -r 4606a9cadd83 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue May 25 23:00:29 2021 +0200
+++ b/src/Pure/Thy/latex.scala	Tue May 25 23:04:29 2021 +0200
@@ -15,19 +15,6 @@
 
 object Latex
 {
-  /** latex errors **/
-
-  def latex_errors(dir: Path, root_name: String): List[String] =
-  {
-    val root_log_path = dir + Path.explode(root_name).ext("log")
-    if (root_log_path.is_file) {
-      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
-      yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
-    }
-    else Nil
-  }
-
-
   /* output text and positions */
 
   type Text = XML.Body
@@ -117,6 +104,16 @@
 
   /* latex log */
 
+  def latex_errors(dir: Path, root_name: String): List[String] =
+  {
+    val root_log_path = dir + Path.explode(root_name).ext("log")
+    if (root_log_path.is_file) {
+      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
+        yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
+    }
+    else Nil
+  }
+
   def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
   {
     val seen_files = Synchronized(Map.empty[JFile, Tex_File])