# HG changeset patch # User wenzelm # Date 1673732235 -3600 # Node ID ac92a7c948b147175889880d50990ff0f835f5d2 # Parent f33e7d80aacebbf82f316331ae8e997bad208e41 tuned; diff -r f33e7d80aace -r ac92a7c948b1 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) }