# HG changeset patch # User wenzelm # Date 1673723709 -3600 # Node ID 6c542f2aab85d346559d6ba907cdfc485c7eec6b # Parent d1776c5ddc93e6f3cc8bc228a4a2b332034dcf8c basic support for update_cite_commands; diff -r d1776c5ddc93 -r 6c542f2aab85 etc/options --- 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" diff -r d1776c5ddc93 -r 6c542f2aab85 src/Pure/Thy/bibtex.scala --- 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 + """>\""" + body + """\""" + + 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("""\""", """\ in""") + Regex.quoteReplacement(cite_antiquotation(name, body2)) + }) + str2 + } } diff -r d1776c5ddc93 -r 6c542f2aab85 src/Pure/Tools/update.scala --- 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)