src/Pure/Thy/document_build.scala
changeset 77025 34219d664854
parent 77018 5292286908a4
child 77173 f1063cdb0093
--- a/src/Pure/Thy/document_build.scala	Fri Jan 20 13:31:58 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Jan 20 13:42:39 2023 +0100
@@ -240,7 +240,15 @@
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
             YXML.parse_body(entry.text)
           }
-          else Nil
+          else {
+            val text =
+              proper_string(session_context.theory_source(name.theory)) getOrElse
+                File.read(name.path)
+            (for {
+              outer <- Bibtex.Cite.parse(Bibtex.cite_commands(options), text)
+              inner <- outer.parse
+            } yield inner.nocite.latex_text).flatten
+          }
 
         def line_pos(props: Properties.T): Option[Int] =
           Position.Line.unapply(props) orElse {