src/Pure/Tools/bibtex.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Tools/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 cite_macro} (K "cite");
+
+val _ =
+  Theory.setup
+   (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
+    Thy_Output.antiquotation @{binding cite}
+      (Scan.lift
+        (Scan.option (Parse.verbatim || Parse.cartouche) --
+         Scan.repeat1 (Parse.position Args.name)))
+      (fn {context = ctxt, ...} => fn (opt, cites) =>
+        let
+          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
+          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
+          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
+        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
+
+end;
+