src/Pure/Thy/bibtex.ML

clarified Latex markup: optional cite "location" consists of nested document text;

(*  Title:      Pure/Thy/bibtex.ML
    Author:     Makarius

BibTeX support.
*)

signature BIBTEX =
sig
  val check_database:
    Position.T -> string -> (string * Position.T) list * (string * Position.T) list
  val check_database_output: Position.T -> string -> unit
  val cite_macro: string Config.T
end;

structure Bibtex: BIBTEX =
struct

(* check database *)

type message = string * Position.T;

fun check_database pos0 database =
  \<^scala>\<open>bibtex_check_database\<close> database
  |> YXML.parse_body
  |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
  |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));

fun check_database_output pos0 database =
  let val (errors, warnings) = check_database pos0 database in
    errors |> List.app (fn (msg, pos) =>
      Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
    warnings |> List.app (fn (msg, pos) =>
      warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
  end;


(* document antiquotations *)

val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");

val _ =
  Theory.setup
   (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
    Document_Output.antiquotation_raw \<^binding>\<open>cite\<close>
      (Scan.lift (Scan.option Args.cartouche_input -- Parse.and_list1 Args.name_position))
      (fn ctxt => fn (opt_loc, citations) =>
        let
          val loc = the_default Input.empty opt_loc;
          val _ =
            Context_Position.reports ctxt
              (Document_Output.document_reports loc @
                map (fn (name, pos) => (pos, Markup.citation name)) citations);

          val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
          val bibtex_entries = Resources.theory_bibtex_entries thy_name;
          val _ =
            if null bibtex_entries andalso thy_name <> Context.PureN then ()
            else
              citations |> List.app (fn (name, pos) =>
                if member (op =) bibtex_entries name then ()
                else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));

          val kind = Config.get ctxt cite_macro;
          val location = Document_Output.output_document ctxt {markdown = false} loc;
        in Latex.cite {kind = kind, citations = citations, location = location} end));

end;