--- 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 =>
--- 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
--- 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 {