tuned;
authorwenzelm
Sat, 14 Jan 2023 22:37:15 +0100
changeset 76977 ac92a7c948b1
parent 76976 f33e7d80aace
child 76978 d60dbb325535
tuned;
src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Jan 14 22:24:01 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sat Jan 14 22:37:15 2023 +0100
@@ -12,8 +12,8 @@
     Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)
 
   def update_xml(options: Options, xml: XML.Body): XML.Body = {
-    val path_cartouches = options.bool("update_path_cartouches")
-    val cite_commands = options.bool("update_cite_commands")
+    val update_path_cartouches = options.bool("update_path_cartouches")
+    val update_cite_commands = options.bool("update_cite_commands")
 
     def upd(lang: Markup.Language, ts: XML.Body): XML.Body =
       ts flatMap {
@@ -21,7 +21,7 @@
           val body = if (markup.name == Markup.UPDATE) body1 else body2
           upd(lang, body)
         case XML.Elem(Markup.Language(lang1), body) =>
-          if (lang1.is_path && path_cartouches) {
+          if (update_path_cartouches && lang1.is_path) {
             Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
               case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
               case None => upd(lang1, body)
@@ -29,7 +29,8 @@
           }
           else upd(lang1, body)
         case XML.Elem(_, body) => upd(lang, body)
-        case XML.Text(s) if (lang.is_document || lang.is_antiquotation) && cite_commands =>
+        case XML.Text(s)
+        if update_cite_commands && (lang.is_document || lang.is_antiquotation) =>
           List(XML.Text(Bibtex.update_cite(s)))
         case t => List(t)
       }