basic support for update_cite_commands;

--- a/etc/options	Sat Jan 14 19:47:02 2023 +0100
+++ b/etc/options	Sat Jan 14 20:15:09 2023 +0100
@@ -346,6 +346,9 @@
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
+option update_cite_commands : bool = false
+  -- "update cite commands and antiquotations"
+
 
 section "Build Database"
 

--- a/src/Pure/Thy/bibtex.scala	Sat Jan 14 19:47:02 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Sat Jan 14 20:15:09 2023 +0100
@@ -12,6 +12,7 @@
 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
+import scala.util.matching.Regex
 
 
 object Bibtex {
@@ -715,4 +716,47 @@
       else html
     }
   }
+
+
+
+  /** cite commands and antiquotations **/
+
+  def cite_antiquotation(name: String, body: String): String =
+    """\<^""" + name + """>\<open>""" + body + """\<close>"""
+
+  def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
+    val body =
+      (if (location.isEmpty) "" else Symbol.cartouche(location) + " in ") +
+      citations.map(quote).mkString(" and ")
+    cite_antiquotation(name, body)
+  }
+
+  private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
+  private val Cite_Antiq = """@\{cite\s*([^}]*)\}""".r
+  private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
+
+  def update_cite(str: String): String = {
+    val str1 =
+      Cite_Command.replaceAllIn(str, { m =>
+        val name = m.group(1)
+        val loc = m.group(2)
+        val location =
+          if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
+          else loc
+        val citations = Library.space_explode(',', m.group(3)).map(_.trim)
+        Regex.quoteReplacement(cite_antiquotation(name, location, citations))
+      })
+    val str2 =
+      Cite_Antiq.replaceAllIn(str1, { m =>
+        val body0 = m.group(1)
+        val (name, body1) =
+          Cite_Macro.findFirstMatchIn(body0) match {
+            case None => ("cite", body0)
+            case Some(m1) => (m1.group(1), Cite_Macro.replaceAllIn(body0, ""))
+          }
+        val body2 = body1.replace("""\<close>""", """\<close> in""")
+        Regex.quoteReplacement(cite_antiquotation(name, body2))
+      })
+    str2
+  }
 }

--- a/src/Pure/Tools/update.scala	Sat Jan 14 19:47:02 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sat Jan 14 20:15:09 2023 +0100
@@ -13,6 +13,7 @@
 
   def update_xml(options: Options, xml: XML.Body): XML.Body = {
     val path_cartouches = options.bool("update_path_cartouches")
+    val cite_commands = options.bool("update_cite_commands")
 
     def upd(lang: Markup.Language, ts: XML.Body): XML.Body =
       ts flatMap {
@@ -28,6 +29,8 @@
           }
           else upd(lang1, body)
         case XML.Elem(_, body) => upd(lang, body)
+        case XML.Text(s) if lang.is_document && cite_commands =>
+          List(XML.Text(Bibtex.update_cite(s)))
         case t => List(t)
       }
     upd(Markup.Language.outer, xml)