src/Pure/Tools/bibtex.ML
author wenzelm
Sun Oct 05 16:05:17 2014 +0200 (2014-10-05)
changeset 58544 340f130b3d38
child 58545 30b75b7958d6
permissions -rw-r--r--
bibtex support in ML: document antiquotation @{cite} with markup;
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@58544
    23
         Scan.repeat1 (Parse.position Args.name)))
wenzelm@58544
    24
      (fn {context = ctxt, ...} => fn (opt, cites) =>
wenzelm@58544
    25
        let
wenzelm@58544
    26
          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
wenzelm@58544
    27
          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
wenzelm@58544
    28
          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
wenzelm@58544
    29
        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
wenzelm@58544
    30
wenzelm@58544
    31
end;
wenzelm@58544
    32