| author | haftmann |
| Thu, 03 Dec 2015 15:33:01 +0100 | |
| changeset 61781 | e1e6bb36b27a |
| parent 58550 | f65911a725ba |
| child 65032 | 42b92fa72a51 |
| permissions | -rw-r--r-- |
|
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 |
|
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
15 |
val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
|
|
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 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
19 |
(Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
|
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
20 |
Thy_Output.antiquotation @{binding cite}
|
|
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; |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
34 |