clarified names;
authorwenzelm
Sun, 15 Jan 2023 12:07:08 +0100
changeset 76981 7ca7343af00e
parent 76980 5e34a2866edb
child 76982 6106c5b4e6eb
clarified names;
etc/options
src/Pure/Tools/update.scala
--- a/etc/options	Sun Jan 15 12:04:08 2023 +0100
+++ b/etc/options	Sun Jan 15 12:07:08 2023 +0100
@@ -346,7 +346,7 @@
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
-option update_cite_commands : bool = false
+option update_cite : bool = false
   -- "update cite commands and antiquotations"
 
 
--- a/src/Pure/Tools/update.scala	Sun Jan 15 12:04:08 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sun Jan 15 12:07:08 2023 +0100
@@ -13,7 +13,7 @@
 
   def update_xml(options: Options, xml: XML.Body): XML.Body = {
     val update_path_cartouches = options.bool("update_path_cartouches")
-    val update_cite_commands = options.bool("update_cite_commands")
+    val update_cite = options.bool("update_cite")
 
     def upd(lang: Markup.Language, ts: XML.Body): XML.Body =
       ts flatMap {
@@ -30,7 +30,7 @@
           else upd(lang1, body)
         case XML.Elem(_, body) => upd(lang, body)
         case XML.Text(s)
-        if update_cite_commands && (lang.is_document || lang.is_antiquotation) =>
+        if update_cite && (lang.is_document || lang.is_antiquotation) =>
           List(XML.Text(Bibtex.update_cite(s)))
         case t => List(t)
       }