tuned;
authorwenzelm
Sat, 14 Jan 2023 17:52:12 +0100
changeset 76968 fd4195298eff
parent 76967 38e19412cf31
child 76969 d1fbd04a976e
tuned;
src/Pure/Tools/update.scala
--- 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)
       }