--- 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 + """>\<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_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("""\<close>""", """\<close> 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 + """>\<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_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("""\<close>""", """\<close> in""")
+ if (cite_commands.contains(name)) cite_antiquotation(name, body2)
+ else cite_antiquotation(CITE, body2 + " using " + quote(name))
+ }
+ }
}