src/Pure/Tools/bibtex.ML
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65032 42b92fa72a51
child 67147 dea94b1aabc3
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Tools/bibtex.ML
     2     Author:     Makarius
     3 
     4 BibTeX support.
     5 *)
     6 
     7 signature BIBTEX =
     8 sig
     9   val cite_macro: string Config.T
    10 end;
    11 
    12 structure Bibtex: BIBTEX =
    13 struct
    14 
    15 val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
    16 
    17 val _ =
    18   Theory.setup
    19    (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
    20     Thy_Output.antiquotation @{binding cite}
    21       (Scan.lift
    22         (Scan.option (Parse.verbatim || Parse.cartouche) --
    23          Parse.and_list1 (Parse.position Args.name)))
    24       (fn {context = ctxt, ...} => fn (opt, citations) =>
    25         let
    26           val _ =
    27             Context_Position.reports ctxt
    28               (map (fn (name, pos) => (pos, Markup.citation name)) citations);
    29           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
    30           val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
    31         in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
    32 
    33 end;