equal
deleted
inserted
replaced
45 (Scan.lift |
45 (Scan.lift |
46 (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) |
46 (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) |
47 (fn ctxt => fn (opt, citations) => |
47 (fn ctxt => fn (opt, citations) => |
48 let |
48 let |
49 val thy = Proof_Context.theory_of ctxt; |
49 val thy = Proof_Context.theory_of ctxt; |
50 val bibtex_entries = Present.get_bibtex_entries thy; |
50 val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy); |
51 val _ = |
51 val _ = |
52 if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () |
52 if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () |
53 else |
53 else |
54 citations |> List.app (fn (name, pos) => |
54 citations |> List.app (fn (name, pos) => |
55 if member (op =) bibtex_entries name then () |
55 if member (op =) bibtex_entries name then () |