# HG changeset patch
# User wenzelm
# Date 1673731441 -3600
# Node ID f33e7d80aacebbf82f316331ae8e997bad208e41
# Parent  5ba8cb258e75eae3f42dad71e5b970b30d7ddbab
proper language context;

diff -r 5ba8cb258e75 -r f33e7d80aace src/Pure/PIDE/markup.scala
--- 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))
diff -r 5ba8cb258e75 -r f33e7d80aace src/Pure/Tools/update.scala
--- 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)