# HG changeset patch
# User wenzelm
# Date 1674125181 -3600
# Node ID 9107e103754ce8491791058580ae22a458d9a376
# Parent  f016a8d99fc9bccea37cc2e0f110d098d6d732bc
clarified signature;

diff -r f016a8d99fc9 -r 9107e103754c src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu Jan 19 11:42:01 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Jan 19 11:46:21 2023 +0100
@@ -723,6 +723,15 @@
 
   /** cite commands and antiquotations **/
 
+  /* cite commands */
+
+  def cite_commands(options: Options): List[String] =
+    Library.space_explode(',', options.string("document_cite_commands"))
+
+  val CITE = "cite"
+  val NOCITE = "nocite"
+
+
   /* update old forms */
 
   def cite_antiquotation(name: String, body: String): String =
@@ -737,8 +746,6 @@
 
   private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
   private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
-  private val CITE = "cite"
-  private val NOCITE = "nocite"
 
   def update_cite_commands(str: String): String =
     Cite_Command.replaceAllIn(str, { m =>
diff -r f016a8d99fc9 -r 9107e103754c src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Thu Jan 19 11:42:01 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Jan 19 11:46:21 2023 +0100
@@ -53,7 +53,7 @@
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
-          val kind = Markup.Kind.unapply(props).getOrElse("cite")
+          val kind = Markup.Kind.unapply(props).getOrElse(Bibtex.CITE)
           val citations = Markup.Citations.get(props)
           Some(Value(kind, citations, body))
         case _ => None
diff -r f016a8d99fc9 -r 9107e103754c src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Thu Jan 19 11:42:01 2023 +0100
+++ b/src/Pure/Tools/update.scala	Thu Jan 19 11:46:21 2023 +0100
@@ -14,7 +14,7 @@
   def update_xml(options: Options, xml: XML.Body): XML.Body = {
     val update_path_cartouches = options.bool("update_path_cartouches")
     val update_cite = options.bool("update_cite")
-    val cite_commands = Library.space_explode(',', options.string("document_cite_commands"))
+    val cite_commands = Bibtex.cite_commands(options)
 
     def upd(lang: Markup.Language, ts: XML.Body): XML.Body =
       ts flatMap {