src/Pure/Tools/bibtex.ML
author wenzelm
Sun Oct 05 17:58:36 2014 +0200 (2014-10-05 ago)
changeset 58545 30b75b7958d6
parent 58544 340f130b3d38
child 58550 f65911a725ba
permissions -rw-r--r--
citation tooltip/hyperlink based on open buffers with .bib files;
     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          Scan.repeat1 (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;
    34