--- a/src/Pure/PIDE/markup.scala Sat Jan 14 22:23:40 2023 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Jan 14 22:24:01 2023 +0100
@@ -188,6 +188,7 @@
val LANGUAGE = "language"
object Language {
val DOCUMENT = "document"
+ val ANTIQUOTATION = "antiquotation"
val ML = "ML"
val SML = "SML"
val PATH = "path"
@@ -218,6 +219,7 @@
override def toString: String = name
def is_document: Boolean = name == Language.DOCUMENT
+ def is_antiquotation: Boolean = name == Language.ANTIQUOTATION
def is_path: Boolean = name == Language.PATH
def description: String = Word.implode(Word.explode('_', name))
--- a/src/Pure/Tools/update.scala Sat Jan 14 22:23:40 2023 +0100
+++ b/src/Pure/Tools/update.scala Sat Jan 14 22:24:01 2023 +0100
@@ -29,7 +29,7 @@
}
else upd(lang1, body)
case XML.Elem(_, body) => upd(lang, body)
- case XML.Text(s) if lang.is_document && cite_commands =>
+ case XML.Text(s) if (lang.is_document || lang.is_antiquotation) && cite_commands =>
List(XML.Text(Bibtex.update_cite(s)))
case t => List(t)
}
@@ -108,7 +108,7 @@
if snapshot.node.source_wellformed
} {
progress.expose_interrupt()
- val xml = snapshot.xml_markup(elements = update_elements)
+ val xml = YXML.parse_body(YXML.string_of_body(snapshot.xml_markup(elements = update_elements)))
val source1 = XML.content(update_xml(session_options, xml))
if (source1 != snapshot.node.source) {
val path = Path.explode(node_name.node)