# HG changeset patch
# User wenzelm
# Date 1673970987 -3600
# Node ID ffc0774e0efe86d419813aab7c72ca675a337915
# Parent  ff203584b36ee879d21b831548c2047bed63a757
clarified file positions: retain original source path;

diff -r ff203584b36e -r ffc0774e0efe src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jan 17 16:08:54 2023 +0100
+++ b/src/Pure/General/path.scala	Tue Jan 17 16:56:27 2023 +0100
@@ -220,6 +220,11 @@
   def is_java: Boolean = ends_with(".java")
   def is_scala: Boolean = ends_with(".scala")
   def is_pdf: Boolean = ends_with(".pdf")
+  def is_latex: Boolean =
+    ends_with(".tex") ||
+    ends_with(".sty") ||
+    ends_with(".cls") ||
+    ends_with(".clo")
 
   def ext(e: String): Path =
     if (e == "") this
diff -r ff203584b36e -r ffc0774e0efe src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Jan 17 16:08:54 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Tue Jan 17 16:56:27 2023 +0100
@@ -264,16 +264,14 @@
 
       /* actual sources: with SHA1 digest */
 
-      isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
+      isabelle_styles.foreach(Latex.copy_file(_, doc_dir))
 
       val comment_latex = latex_output.options.bool("document_comment_latex")
-      if (!comment_latex) {
-        Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir)
-      }
+      if (!comment_latex) Latex.copy_file(texinputs + Path.basic("comment.sty"), doc_dir)
       doc.tags.sty(comment_latex).write(doc_dir)
 
       for ((base_dir, src) <- info.document_files) {
-        Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
+        Latex.copy_file_base(info.dir + base_dir, src, doc_dir)
       }
 
       session_tex.write(doc_dir)
@@ -435,7 +433,7 @@
 
     override def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = {
       val doc_dir = context.make_directory(dir, doc)
-      Build_LIPIcs.document_files.foreach(Isabelle_System.copy_file(_, doc_dir))
+      Build_LIPIcs.document_files.foreach(Latex.copy_file(_, doc_dir))
 
       val latex_output = new Latex.Output(lipics_options(context.options))
       context.prepare_directory(dir, doc, latex_output)
diff -r ff203584b36e -r ffc0774e0efe src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue Jan 17 16:08:54 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Tue Jan 17 16:56:27 2023 +0100
@@ -172,6 +172,31 @@
     if (file_pos.isEmpty) Nil
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
+  def append_position(path: Path, file_pos: String): Unit = {
+    val pos = init_position(file_pos).mkString
+    if (pos.nonEmpty) {
+      val sep = if (File.read(path).endsWith("\n")) "" else "\n"
+      File.append(path, sep + pos)
+    }
+  }
+
+  def copy_file(src: Path, dst: Path): Unit = {
+    Isabelle_System.copy_file(src, dst)
+    if (src.is_latex) {
+      val target = if (dst.is_dir) dst + src.base else dst
+      val file_pos = File.symbolic_path(src)
+      append_position(target, file_pos)
+    }
+  }
+
+  def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
+    Isabelle_System.copy_file_base(base_dir, src, target_dir)
+    if (src.is_latex) {
+      val file_pos = File.symbolic_path(base_dir + src)
+      append_position(target_dir + src, file_pos)
+    }
+  }
+
   class Output(val options: Options) {
     def latex_output(latex_text: Text): String = make(latex_text)
 
@@ -335,7 +360,8 @@
       }
 
     def position(line: Int): Position.T =
-      source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
+      source_position(line) getOrElse
+        Position.Line_File(line, source_file.getOrElse(tex_file.implode))
   }