# HG changeset patch # User wenzelm # Date 1673796483 -3600 # Node ID 1e31ddcab458785aa9ad39fcef387ad342ce8813 # Parent aafe49b6320579ec19a38cab45c6c0485b15c515 clarified treatment of cite macro name; diff -r aafe49b63205 -r 1e31ddcab458 NEWS --- a/NEWS Sun Jan 15 15:30:25 2023 +0100 +++ b/NEWS Sun Jan 15 16:28:03 2023 +0100 @@ -33,6 +33,9 @@ \<^cite>\"isabelle-system" and "isabelle-jedit"\ \<^nocite>\"isabelle-isar-ref"\ +The old antiquotation option "cite_macro" has been superseded by +explicit syntax: \<^cite>\\ using macro_name\. + The command-line tool "isabelle update -u cite" helps to update former uses of LaTeX \cite commands and old-style @{cite "name"} document antiquotations. diff -r aafe49b63205 -r 1e31ddcab458 etc/options --- a/etc/options Sun Jan 15 15:30:25 2023 +0100 +++ b/etc/options Sun Jan 15 16:28:03 2023 +0100 @@ -25,6 +25,8 @@ -- "prefix for LaTeX macros generated from 'chapter', 'section' etc." option document_comment_latex : bool = false -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version" +option document_cite_commands : string = "cite,nocite,citet,citep" + -- "antiquotation commands to determine the structure of bibliography" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" diff -r aafe49b63205 -r 1e31ddcab458 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Jan 15 15:30:25 2023 +0100 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Jan 15 16:28:03 2023 +0100 @@ -348,18 +348,17 @@ \<^descr> \@{cite arg}\ produces the Bib{\TeX} citation macro \<^verbatim>\\cite[...]{...}\ with its optional and mandatory argument. The analogous \<^verbatim>\\nocite\, and the \<^verbatim>\\citet\ and \<^verbatim>\\citep\ variants from the \<^verbatim>\natbib\ - package\<^footnote>\\<^url>\https://ctan.org/pkg/natbib\\ are supported as well. Further - versions can be defined easily in Isabelle/ML, by imitating the ML - definitions behind the existing antiquotations. + package\<^footnote>\\<^url>\https://ctan.org/pkg/natbib\\ are supported as well. The argument syntax is uniform for all variants and is usually presented in control-symbol-cartouche form: \\<^cite>\arg\\. The formal syntax of the nested argument language is defined as follows: \<^rail>\arg: (embedded - @'in')? (name + 'and')\ + @'in')? (name + 'and') \ (@'using' name)?\ Here the embedded text is free-form {\LaTeX}, which becomes the optional argument of the \<^verbatim>\\cite\ macro. The named items are Bib{\TeX} database - entries and become the mandatory argument (separated by comma). + entries and become the mandatory argument (separated by comma). The optional + part ``\<^theory_text>\using name\'' specifies an alternative {\LaTeX} macro name. The validity of Bib{\TeX} database entries is only partially checked in Isabelle/PIDE, when the corresponding \<^verbatim>\.bib\ files are open. Ultimately, diff -r aafe49b63205 -r 1e31ddcab458 src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Sun Jan 15 15:30:25 2023 +0100 +++ b/src/Pure/Thy/bibtex.ML Sun Jan 15 16:28:03 2023 +0100 @@ -48,7 +48,7 @@ val parse_citations = Parse.and_list1 Args.name_position; -fun cite_command ctxt get_kind (opt_loc, citations) = +fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) = let val loc = the_default Input.empty opt_loc; val _ = @@ -65,7 +65,7 @@ if member (op =) bibtex_entries name orelse name = "*" then () else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); - val kind = get_kind ctxt; + val kind = if macro_name = "" then get_kind ctxt else macro_name; val location = Document_Output.output_document ctxt {markdown = false} loc; in Latex.cite {kind = kind, citations = citations, location = location} end; @@ -76,12 +76,14 @@ legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^ Position.here_list (map snd (snd args))) else (); - in cite_command ctxt get_kind args end; + in cite_command ctxt get_kind (args, "") end; fun cite_command_embedded ctxt get_kind input = let - val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt); - val parser = Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations; + val keywords = Thy_Header.get_keywords' ctxt; + val parser = + Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations -- + Scan.optional (Parse.command_name "using" |-- Parse.!!! Parse.name) ""; val args = Parse.read_embedded ctxt keywords parser input; in cite_command ctxt get_kind args end; diff -r aafe49b63205 -r 1e31ddcab458 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Sun Jan 15 15:30:25 2023 +0100 +++ b/src/Pure/Thy/bibtex.scala Sun Jan 15 16:28:03 2023 +0100 @@ -733,6 +733,7 @@ private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r + private val CITE = "cite" def update_cite_commands(str: String): String = Cite_Command.replaceAllIn(str, { m => @@ -745,7 +746,7 @@ Regex.quoteReplacement(cite_antiquotation(name, location, citations)) }) - def update_cite_antiquotation(str: String): String = { + def update_cite_antiquotation(cite_commands: List[String], str: String): String = { val opt_body = for { str1 <- Library.try_unprefix("@{cite", str) @@ -757,11 +758,12 @@ case Some(body0) => val (name, body1) = Cite_Macro.findFirstMatchIn(body0) match { - case None => ("cite", body0) + case None => (CITE, body0) case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, "")) } val body2 = body1.replace("""\""", """\ in""") - cite_antiquotation(name, body2) + if (cite_commands.contains(name)) cite_antiquotation(name, body2) + else cite_antiquotation(CITE, body2 + " using " + quote(name)) } } } diff -r aafe49b63205 -r 1e31ddcab458 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Sun Jan 15 15:30:25 2023 +0100 +++ b/src/Pure/Tools/update.scala Sun Jan 15 16:28:03 2023 +0100 @@ -14,6 +14,7 @@ def update_xml(options: Options, xml: XML.Body): XML.Body = { val update_path_cartouches = options.bool("update_path_cartouches") val update_cite = options.bool("update_cite") + val cite_commands = Library.space_explode(',', options.string("document_cite_commands")) def upd(lang: Markup.Language, ts: XML.Body): XML.Body = ts flatMap { @@ -28,7 +29,7 @@ } } else if (update_cite && lang1.is_antiquotation) { - List(XML.Text(Bibtex.update_cite_antiquotation(XML.content(body)))) + List(XML.Text(Bibtex.update_cite_antiquotation(cite_commands, XML.content(body)))) } else upd(lang1, body) case XML.Elem(_, body) => upd(lang, body)