# HG changeset patch
# User wenzelm
# Date 1673793025 -3600
# Node ID aafe49b6320579ec19a38cab45c6c0485b15c515
# Parent  29432d4a376dd49f6b233805114076d3aa5c1d54
explicit legacy_feature;

diff -r 29432d4a376d -r aafe49b63205 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sun Jan 15 12:55:23 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Sun Jan 15 15:30:25 2023 +0100
@@ -69,6 +69,15 @@
     val location = Document_Output.output_document ctxt {markdown = false} loc;
   in Latex.cite {kind = kind, citations = citations, location = location} end;
 
+fun cite_command_old ctxt get_kind args =
+  let
+    val _ =
+      if Context_Position.is_visible ctxt then
+        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;
+
 fun cite_command_embedded ctxt get_kind input =
   let
     val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt);
@@ -78,7 +87,7 @@
 
 fun cite_command_parser get_kind =
   Scan.option Args.cartouche_input -- parse_citations
-    >> (fn args => fn ctxt => cite_command ctxt get_kind args) ||
+    >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
   Parse.embedded_input
     >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);