# HG changeset patch
# User wenzelm
# Date 1673609829 -3600
# Node ID 3d491a0af6ef01e5f50486559806a3981d49acf8
# Parent  d9727629cb67efb107d7bb06c4ac6b7aa6d5fd55
clarified signature: more generic operations;

diff -r d9727629cb67 -r 3d491a0af6ef src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Fri Jan 13 12:16:04 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 13 12:37:09 2023 +0100
@@ -10,6 +10,7 @@
     Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
   val cite_macro: string Config.T
+  val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
 end;
 
 structure Bibtex: BIBTEX =
@@ -38,30 +39,33 @@
 
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
 
+fun cite_antiquotation binding get_kind =
+  Document_Output.antiquotation_raw binding
+    (Scan.lift (Scan.option Args.cartouche_input -- Parse.and_list1 Args.name_position))
+    (fn ctxt => fn (opt_loc, citations) =>
+      let
+        val loc = the_default Input.empty opt_loc;
+        val _ =
+          Context_Position.reports ctxt
+            (Document_Output.document_reports loc @
+              map (fn (name, pos) => (pos, Markup.citation name)) citations);
+
+        val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
+        val bibtex_entries = Resources.theory_bibtex_entries thy_name;
+        val _ =
+          if null bibtex_entries andalso thy_name <> Context.PureN then ()
+          else
+            citations |> List.app (fn (name, pos) =>
+              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 location = Document_Output.output_document ctxt {markdown = false} loc;
+      in Latex.cite {kind = kind, citations = citations, location = location} end);
+
 val _ =
   Theory.setup
    (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
-    Document_Output.antiquotation_raw \<^binding>\<open>cite\<close>
-      (Scan.lift (Scan.option Args.cartouche_input -- Parse.and_list1 Args.name_position))
-      (fn ctxt => fn (opt_loc, citations) =>
-        let
-          val loc = the_default Input.empty opt_loc;
-          val _ =
-            Context_Position.reports ctxt
-              (Document_Output.document_reports loc @
-                map (fn (name, pos) => (pos, Markup.citation name)) citations);
-
-          val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
-          val bibtex_entries = Resources.theory_bibtex_entries thy_name;
-          val _ =
-            if null bibtex_entries andalso thy_name <> Context.PureN then ()
-            else
-              citations |> List.app (fn (name, pos) =>
-                if member (op =) bibtex_entries name orelse name = "*" then ()
-                else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
-
-          val kind = Config.get ctxt cite_macro;
-          val location = Document_Output.output_document ctxt {markdown = false} loc;
-        in Latex.cite {kind = kind, citations = citations, location = location} end));
+    cite_antiquotation \<^binding>\<open>cite\<close> (fn ctxt => Config.get ctxt cite_macro));
 
 end;