# HG changeset patch
# User wenzelm
# Date 1673783723 -3600
# Node ID 29432d4a376dd49f6b233805114076d3aa5c1d54
# Parent  90fea73f051d37d61462e76021d135bd9bf3f349
more robust: rely on PIDE markup instead of regex guess;

diff -r 90fea73f051d -r 29432d4a376d src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sun Jan 15 12:13:19 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Sun Jan 15 12:55:23 2023 +0100
@@ -732,31 +732,36 @@
   }
 
   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)
+  def update_cite_commands(str: String): String =
+    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))
+    })
+
+  def update_cite_antiquotation(str: String): String = {
+    val opt_body =
+      for {
+        str1 <- Library.try_unprefix("@{cite", str)
+        str2 <- Library.try_unsuffix("}", str1)
+      } yield str2.trim
+
+    opt_body match {
+      case None => str
+      case Some(body0) =>
         val (name, body1) =
           Cite_Macro.findFirstMatchIn(body0) match {
             case None => ("cite", body0)
-            case Some(m1) => (m1.group(1), Cite_Macro.replaceAllIn(body0, ""))
+            case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, ""))
           }
         val body2 = body1.replace("""\<close>""", """\<close> in""")
-        Regex.quoteReplacement(cite_antiquotation(name, body2))
-      })
-    str2
+        cite_antiquotation(name, body2)
+    }
   }
 }
diff -r 90fea73f051d -r 29432d4a376d src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sun Jan 15 12:13:19 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sun Jan 15 12:55:23 2023 +0100
@@ -27,11 +27,13 @@
               case None => upd(lang1, body)
             }
           }
+          else if (update_cite && lang1.is_antiquotation) {
+            List(XML.Text(Bibtex.update_cite_antiquotation(XML.content(body))))
+          }
           else upd(lang1, body)
         case XML.Elem(_, body) => upd(lang, body)
-        case XML.Text(s)
-        if update_cite && (lang.is_document || lang.is_antiquotation) =>
-          List(XML.Text(Bibtex.update_cite(s)))
+        case XML.Text(s) if update_cite && lang.is_document =>
+          List(XML.Text(Bibtex.update_cite_commands(s)))
         case t => List(t)
       }
     upd(Markup.Language.outer, xml)