--- a/src/Pure/Tools/update.scala Fri Jan 13 19:16:24 2023 +0100
+++ b/src/Pure/Tools/update.scala Sat Jan 14 17:52:12 2023 +0100
@@ -67,14 +67,14 @@
case XML.Wrapped_Elem(markup, body1, body2) =>
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) {
+ case XML.Elem(Markup.Language(lang1), body) =>
+ if (lang1.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 None => update_xml(lang1, body)
}
}
- else update_xml(lang, body)
+ else update_xml(lang1, body)
case XML.Elem(_, body) => update_xml(lang, body)
case t => List(t)
}