merged

--- a/src/HOL/Analysis/Infinite_Sum.thy	Thu Jan 19 11:13:45 2023 +0000
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Thu Jan 19 11:13:52 2023 +0000
@@ -9,13 +9,6 @@
 section \<open>Infinite sums\<close>
 \<^latex>\<open>\label{section:Infinite_Sum}\<close>
 
-theory Infinite_Sum
-  imports
-    Elementary_Topology
-    "HOL-Library.Extended_Nonnegative_Real"
-    "HOL-Library.Complex_Order"
-begin
-
 text \<open>In this theory, we introduce the definition of infinite sums, i.e., sums ranging over an
 infinite, potentially uncountable index set with no particular ordering.
 (This is different from series. Those are sums indexed by natural numbers,
@@ -29,6 +22,12 @@
 commutative monoid endowed with a Hausdorff topology.
 (Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
 
+theory Infinite_Sum
+  imports
+    Elementary_Topology
+    "HOL-Library.Extended_Nonnegative_Real"
+    "HOL-Library.Complex_Order"
+begin
 
 subsection \<open>Definition and syntax\<close>
 

--- a/src/Pure/General/path.scala	Thu Jan 19 11:13:45 2023 +0000
+++ b/src/Pure/General/path.scala	Thu Jan 19 11:13:52 2023 +0000
@@ -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

--- a/src/Pure/Thy/bibtex.ML	Thu Jan 19 11:13:45 2023 +0000
+++ b/src/Pure/Thy/bibtex.ML	Thu Jan 19 11:13:52 2023 +0000
@@ -57,14 +57,17 @@
           map (fn (name, pos) => (pos, Markup.citation name)) citations);
 
     val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
-    val bibtex_entries =
-      if thy_name = Context.PureN then []
-      else Resources.theory_bibtex_entries thy_name;
+    val bibtex_entries = Resources.theory_bibtex_entries thy_name;
     val _ =
       if null bibtex_entries andalso thy_name <> Context.PureN then ()
       else
         citations |> List.app (fn (name, pos) =>
           if member (op =) bibtex_entries name orelse name = "*" then ()
+          else if thy_name = Context.PureN then
+            (if Context_Position.is_visible ctxt then
+               warning ("Missing theory context --- unchecked Bibtex entry " ^
+                 quote name ^ Position.here pos)
+             else ())
           else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
     val kind = if macro_name = "" then get_kind ctxt else macro_name;

--- a/src/Pure/Thy/document_build.scala	Thu Jan 19 11:13:45 2023 +0000
+++ b/src/Pure/Thy/document_build.scala	Thu Jan 19 11:13:52 2023 +0000
@@ -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)

--- a/src/Pure/Thy/latex.scala	Thu Jan 19 11:13:45 2023 +0000
+++ b/src/Pure/Thy/latex.scala	Thu Jan 19 11:13:52 2023 +0000
@@ -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))
   }