# HG changeset patch
# User wenzelm
# Date 1673633238 -3600
# Node ID 2f91b787f509897bed5f6a40912fac142139dd37
# Parent  922df6aa16072251e86b78d0bb65ea5a1a4b0d6d
more explicit language context;

diff -r 922df6aa1607 -r 2f91b787f509 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 13 17:14:59 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 13 19:07:18 2023 +0100
@@ -198,6 +198,8 @@
       def description: String = Word.implode(Word.explode('_', name))
     }
 
+    val outer: Value = Value("", true, false, false)
+
     def unapply(markup: Markup): Option[Value] =
       markup match {
         case Markup(LANGUAGE, props) =>
diff -r 922df6aa1607 -r 2f91b787f509 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 13 17:14:59 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 13 19:07:18 2023 +0100
@@ -62,17 +62,20 @@
 
     val path_cartouches = options.bool("update_path_cartouches")
 
-    def update_xml(xml: XML.Body): XML.Body =
+    def update_xml(lang: Markup.Language.Value, xml: XML.Body): XML.Body =
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
-          if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
-        case XML.Elem(Markup.Language(lang), body)
-        if lang.is_path && path_cartouches =>
-          Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
-            case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
-            case None => update_xml(body)
+          val body = if (markup.name == Markup.UPDATE) body1 else body2
+          update_xml(lang, body)
+        case XML.Elem(Markup.Language(lang), body) =>
+          if (lang.is_path && path_cartouches) {
+            Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
+              case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
+              case None => update_xml(lang, body)
+            }
           }
-        case XML.Elem(_, body) => update_xml(body)
+          else update_xml(lang, body)
+        case XML.Elem(_, body) => update_xml(lang, body)
         case t => List(t)
       }
 
@@ -102,7 +105,7 @@
             } {
               progress.expose_interrupt()
               val source1 =
-                XML.content(update_xml(
+                XML.content(update_xml(Markup.Language.outer,
                   snapshot.xml_markup(elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))))
               if (source1 != snapshot.node.source) {
                 val path = Path.explode(node_name.node)