src/Pure/Thy/bibtex.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/bibtex.ML	Sun Dec 24 13:07:05 2017 +0100
@@ -0,0 +1,33 @@
+(*  Title:      Pure/Thy/bibtex.ML
+    Author:     Makarius
+
+BibTeX support.
+*)
+
+signature BIBTEX =
+sig
+  val cite_macro: string Config.T
+end;
+
+structure Bibtex: BIBTEX =
+struct
+
+val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
+
+val _ =
+  Theory.setup
+   (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
+    Thy_Output.antiquotation \<^binding>\<open>cite\<close>
+      (Scan.lift
+        (Scan.option (Parse.verbatim || Parse.cartouche) --
+         Parse.and_list1 (Parse.position Args.name)))
+      (fn {context = ctxt, ...} => fn (opt, citations) =>
+        let
+          val _ =
+            Context_Position.reports ctxt
+              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
+          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
+          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
+        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
+
+end;