src/Pure/Tools/bibtex.ML
changeset 67274 4588f714a78a
parent 67273 c573cfb2c407
child 67275 5e427586cb57
--- a/src/Pure/Tools/bibtex.ML	Sun Dec 24 12:48:43 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  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>\<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;