author | wenzelm |
Fri, 29 Dec 2017 17:40:57 +0100 | |
changeset 67297 | 86a099f896fc |
parent 67280 | dfc5a1503916 |
child 67301 | e255c76db052 |
permissions | -rw-r--r-- |
67274 | 1 |
(* Title: Pure/Thy/bibtex.ML |
58544
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 |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
9 |
type message = {is_error: bool, msg: string, pos: Position.T} |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
10 |
val check_database: Position.T -> string -> message list |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
11 |
val check_database_output: Position.T -> string -> unit |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
12 |
val cite_macro: string Config.T |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
13 |
end; |
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 |
structure Bibtex: BIBTEX = |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
16 |
struct |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
17 |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
18 |
(* check database *) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
19 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
20 |
type message = {is_error: bool, msg: string, pos: Position.T}; |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
21 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
22 |
fun check_database pos0 database = |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
23 |
Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
24 |
|> YXML.parse_body |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
25 |
|> let open XML.Decode in list (triple bool string properties) end |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
26 |
|> map (fn (is_error, msg, pos) => |
67280
dfc5a1503916
clarified default position for empty message pos;
wenzelm
parents:
67275
diff
changeset
|
27 |
{is_error = is_error, msg = msg, pos = Position.of_properties (pos @ Position.get_props pos0)}); |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
28 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
29 |
fun check_database_output pos0 database = |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
30 |
let |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
31 |
val messages = check_database pos0 database; |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
32 |
val (errors, warnings) = List.partition #is_error messages; |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
33 |
in |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
34 |
errors |> List.app (fn {msg, pos, ...} => |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
35 |
Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
36 |
warnings |> List.app (fn {msg, pos, ...} => |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
37 |
warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
38 |
end; |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
39 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
40 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
41 |
(* document antiquotations *) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
42 |
|
67147 | 43 |
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
|
44 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
45 |
val _ = |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
46 |
Theory.setup |
67147 | 47 |
(Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #> |
48 |
Thy_Output.antiquotation \<^binding>\<open>cite\<close> |
|
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
49 |
(Scan.lift |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
50 |
(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
|
51 |
Parse.and_list1 (Parse.position Args.name))) |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
52 |
(fn {context = ctxt, ...} => fn (opt, citations) => |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
53 |
let |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
54 |
val thy = Proof_Context.theory_of ctxt; |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
55 |
val bibtex_entries = Present.get_bibtex_entries thy; |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
56 |
val _ = |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
57 |
if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
58 |
else |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
59 |
citations |> List.app (fn (name, pos) => |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
60 |
if member (op =) bibtex_entries name then () |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67280
diff
changeset
|
61 |
else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
62 |
val _ = |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
63 |
Context_Position.reports ctxt |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
64 |
(map (fn (name, pos) => (pos, Markup.citation name)) citations); |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
67 |
in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end)); |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
68 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
69 |
end; |