src/Pure/Tools/bibtex.ML
author wenzelm
Wed, 06 Dec 2017 18:59:33 +0100
changeset 67147 dea94b1aabc3
parent 65032 42b92fa72a51
permissions -rw-r--r--
prefer control symbol antiquotations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Tools/bibtex.ML
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     3
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     4
BibTeX support.
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     5
*)
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     6
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     7
signature BIBTEX =
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     8
sig
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
     9
  val cite_macro: string Config.T
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    10
end;
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    11
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    12
structure Bibtex: BIBTEX =
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    13
struct
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    14
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 65032
diff changeset
    15
val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    16
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    17
val _ =
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    18
  Theory.setup
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 65032
diff changeset
    19
   (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 65032
diff changeset
    20
    Thy_Output.antiquotation \<^binding>\<open>cite\<close>
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    21
      (Scan.lift
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    22
        (Scan.option (Parse.verbatim || Parse.cartouche) --
58550
f65911a725ba more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
wenzelm
parents: 58545
diff changeset
    23
         Parse.and_list1 (Parse.position Args.name)))
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
    24
      (fn {context = ctxt, ...} => fn (opt, citations) =>
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    25
        let
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
    26
          val _ =
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
    27
            Context_Position.reports ctxt
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
    28
              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    29
          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
    30
          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    31
        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    32
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff changeset
    33
end;