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