src/Pure/Tools/bibtex.ML
changeset 58550 f65911a725ba
parent 58545 30b75b7958d6
child 65032 42b92fa72a51
equal deleted inserted replaced
58549:d4d97b79f1fb 58550:f65911a725ba
    18   Theory.setup
    18   Theory.setup
    19    (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
    19    (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
    20     Thy_Output.antiquotation @{binding cite}
    20     Thy_Output.antiquotation @{binding cite}
    21       (Scan.lift
    21       (Scan.lift
    22         (Scan.option (Parse.verbatim || Parse.cartouche) --
    22         (Scan.option (Parse.verbatim || Parse.cartouche) --
    23          Scan.repeat1 (Parse.position Args.name)))
    23          Parse.and_list1 (Parse.position Args.name)))
    24       (fn {context = ctxt, ...} => fn (opt, citations) =>
    24       (fn {context = ctxt, ...} => fn (opt, citations) =>
    25         let
    25         let
    26           val _ =
    26           val _ =
    27             Context_Position.reports ctxt
    27             Context_Position.reports ctxt
    28               (map (fn (name, pos) => (pos, Markup.citation name)) citations);
    28               (map (fn (name, pos) => (pos, Markup.citation name)) citations);