src/Pure/Tools/bibtex.ML
changeset 58545 30b75b7958d6
parent 58544 340f130b3d38
child 58550 f65911a725ba
     1.1 --- a/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
     1.2 +++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 17:58:36 2014 +0200
     1.3 @@ -21,11 +21,13 @@
     1.4        (Scan.lift
     1.5          (Scan.option (Parse.verbatim || Parse.cartouche) --
     1.6           Scan.repeat1 (Parse.position Args.name)))
     1.7 -      (fn {context = ctxt, ...} => fn (opt, cites) =>
     1.8 +      (fn {context = ctxt, ...} => fn (opt, citations) =>
     1.9          let
    1.10 -          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
    1.11 +          val _ =
    1.12 +            Context_Position.reports ctxt
    1.13 +              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
    1.14            val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
    1.15 -          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
    1.16 +          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
    1.17          in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
    1.18  
    1.19  end;