# HG changeset patch
# User wenzelm
# Date 1674218559 -3600
# Node ID 34219d664854e67d815c793a8aaba828095171bd
# Parent  6e90e84f7e7ced94f289a42de7f5d8fd7e32020b
proper citations for unselected theories, notably for the default selection of the GUI panel;

diff -r 6e90e84f7e7c -r 34219d664854 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 13:31:58 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 13:42:39 2023 +0100
@@ -748,6 +748,13 @@
     sealed case class Inner(kind: String, citations: String, location: XML.Body, pos: Position.T) {
       def nocite: Inner = copy(kind = NOCITE, location = Nil)
 
+      def latex_text: Latex.Text = {
+        val props =
+          (if (kind.nonEmpty) Markup.Kind(kind) else Nil) :::
+          Markup.Citations(citations) ::: pos
+        List(XML.Elem(Markup.Latex_Cite(props), location))
+      }
+
       override def toString: String = citations
     }
 
diff -r 6e90e84f7e7c -r 34219d664854 src/Pure/Thy/document_build.scala
--- 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 {