# HG changeset patch # User wenzelm # Date 1674212298 -3600 # Node ID 44cd067cecfddb10db8c3a26686c413471326180 # Parent a272cf64bd392b49d3c61f1e0de8ae3a844a3ff0 tuned; diff -r a272cf64bd39 -r 44cd067cecfd src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Thu Jan 19 17:53:05 2023 +0100 +++ b/src/Pure/Thy/bibtex.scala Fri Jan 20 11:58:18 2023 +0100 @@ -732,55 +732,7 @@ val NOCITE = "nocite" - /* update old forms */ - - 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_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r - - 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(cite_commands: List[String], 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(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, "")) - } - val body2 = body1.replace("""\""", """\ in""") - if (cite_commands.contains(name)) cite_antiquotation(name, body2) - else cite_antiquotation(CITE, body2 + " using " + quote(name)) - } - } - - - /* parse within raw source */ + /* citations within theory source */ object Cite { def unapply(tree: XML.Tree): Option[Inner] = @@ -868,4 +820,52 @@ } } } + + + /* update old forms: @{cite ...} and \cite{...} */ + + 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_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r + + 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(cite_commands: List[String], 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(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, "")) + } + val body2 = body1.replace("""\""", """\ in""") + if (cite_commands.contains(name)) cite_antiquotation(name, body2) + else cite_antiquotation(CITE, body2 + " using " + quote(name)) + } + } }