--- 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>\<open>"isabelle-system" and "isabelle-jedit"\<close>
\<^nocite>\<open>"isabelle-isar-ref"\<close>
+The old antiquotation option "cite_macro" has been superseded by
+explicit syntax: \<^cite>\<open>\<dots> using macro_name\<close>.
+
The command-line tool "isabelle update -u cite" helps to update former
uses of LaTeX \cite commands and old-style @{cite "name"} document
antiquotations.
--- 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"
--- 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> \<open>@{cite arg}\<close> produces the Bib{\TeX} citation macro \<^verbatim>\<open>\cite[...]{...}\<close>
with its optional and mandatory argument. The analogous \<^verbatim>\<open>\nocite\<close>, and the
\<^verbatim>\<open>\citet\<close> and \<^verbatim>\<open>\citep\<close> variants from the \<^verbatim>\<open>natbib\<close>
- package\<^footnote>\<open>\<^url>\<open>https://ctan.org/pkg/natbib\<close>\<close> are supported as well. Further
- versions can be defined easily in Isabelle/ML, by imitating the ML
- definitions behind the existing antiquotations.
+ package\<^footnote>\<open>\<^url>\<open>https://ctan.org/pkg/natbib\<close>\<close> are supported as well.
The argument syntax is uniform for all variants and is usually presented in
control-symbol-cartouche form: \<open>\<^cite>\<open>arg\<close>\<close>. The formal syntax of the
nested argument language is defined as follows: \<^rail>\<open>arg: (embedded
- @'in')? (name + 'and')\<close>
+ @'in')? (name + 'and') \<newline> (@'using' name)?\<close>
Here the embedded text is free-form {\LaTeX}, which becomes the optional
argument of the \<^verbatim>\<open>\cite\<close> 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>\<open>using name\<close>'' specifies an alternative {\LaTeX} macro name.
The validity of Bib{\TeX} database entries is only partially checked in
Isabelle/PIDE, when the corresponding \<^verbatim>\<open>.bib\<close> files are open. Ultimately,
--- 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;
--- 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("""\<close>""", """\<close> in""")
- cite_antiquotation(name, body2)
+ if (cite_commands.contains(name)) cite_antiquotation(name, body2)
+ else cite_antiquotation(CITE, body2 + " using " + quote(name))
}
}
}
--- 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)