author | wenzelm |
Sun, 09 Jul 2023 14:33:45 +0200 | |
changeset 78273 | 95a3bb4d7e38 |
parent 77774 | 9273eb5d2672 |
child 78462 | 3023063833e4 |
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 |
67301 | 9 |
val check_database: |
10 |
Position.T -> string -> (string * Position.T) list * (string * Position.T) list |
|
67275
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 |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
12 |
val check_bibtex_entry: Proof.context -> string * Position.T -> unit |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
13 |
val cite_macro: string Config.T |
76959 | 14 |
val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
15 |
end; |
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 |
structure Bibtex: BIBTEX = |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
18 |
struct |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
19 |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
20 |
(* check database *) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
21 |
|
67301 | 22 |
type message = string * Position.T; |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
23 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
24 |
fun check_database pos0 database = |
72194 | 25 |
\<^scala>\<open>bibtex_check_database\<close> database |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
26 |
|> YXML.parse_body |
67301 | 27 |
|> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |
77774 | 28 |
|> (apply2 o map o apsnd) |
29 |
(fn pos => Position.of_properties (pos @ Position.properties_of pos0)); |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
30 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
31 |
fun check_database_output pos0 database = |
67301 | 32 |
let val (errors, warnings) = check_database pos0 database in |
33 |
errors |> List.app (fn (msg, pos) => |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
34 |
Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); |
67301 | 35 |
warnings |> List.app (fn (msg, pos) => |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
36 |
warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
37 |
end; |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
38 |
|
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
39 |
|
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
40 |
(* check bibtex entry *) |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
41 |
|
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
42 |
fun check_bibtex_entry ctxt (name, pos) = |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
43 |
let |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
44 |
fun warn () = |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
45 |
if Context_Position.is_visible ctxt then |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
46 |
warning ("Unknown session context: cannot check Bibtex entry " ^ |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
47 |
quote name ^ Position.here pos) |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
48 |
else (); |
77030
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
49 |
fun decode yxml = |
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
50 |
let |
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
51 |
val props = XML.Decode.properties (YXML.parse_body yxml); |
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
52 |
val name = the_default "" (Properties.get props Markup.nameN); |
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
53 |
val pos = Position.of_properties props; |
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
54 |
in (name, pos) end; |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
55 |
in |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
56 |
if name = "*" then () |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
57 |
else |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
58 |
(case Position.id_of pos of |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
59 |
NONE => warn () |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
60 |
| SOME id => |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
61 |
(case \<^scala>\<open>bibtex_session_entries\<close> [id] of |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
62 |
[] => warn () |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
63 |
| _ :: entries => |
77030
d7dc5b1e4381
proper positions for Isabelle/ML, instead of Isabelle/Scala;
wenzelm
parents:
77029
diff
changeset
|
64 |
Completion.check_entity Markup.bibtex_entryN (map decode entries) |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
65 |
ctxt (name, pos) |> ignore)) |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
66 |
end; |
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
67 |
|
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
68 |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
69 |
(* document antiquotations *) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
70 |
|
76961
d756f4f78dc7
clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
wenzelm
parents:
76960
diff
changeset
|
71 |
val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K ""); |
76963 | 72 |
fun get_cite_macro ctxt = Config.get ctxt cite_macro; |
73 |
||
74 |
val _ = |
|
75 |
Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro)); |
|
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
76 |
|
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
77 |
|
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
78 |
local |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
79 |
|
77033
e75e2f86a6d3
proper position for semantic completion: avoid duplicate quotes;
wenzelm
parents:
77030
diff
changeset
|
80 |
val parse_citations = Parse.and_list1 (Parse.position Parse.name); |
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
81 |
|
76986 | 82 |
fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) = |
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
83 |
let |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
84 |
val loc = the_default Input.empty opt_loc; |
77029
1046a69fabaa
dismantle special treatment of citations in Isabelle/Scala;
wenzelm
parents:
77028
diff
changeset
|
85 |
val _ = Context_Position.reports ctxt (Document_Output.document_reports loc); |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
77027
diff
changeset
|
86 |
val _ = List.app (check_bibtex_entry ctxt) citations; |
76959 | 87 |
|
76986 | 88 |
val kind = if macro_name = "" then get_kind ctxt else macro_name; |
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
89 |
val location = Document_Output.output_document ctxt {markdown = false} loc; |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
90 |
in Latex.cite {kind = kind, citations = citations, location = location} end; |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
91 |
|
76985 | 92 |
fun cite_command_old ctxt get_kind args = |
93 |
let |
|
94 |
val _ = |
|
95 |
if Context_Position.is_visible ctxt then |
|
96 |
legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^ |
|
97 |
Position.here_list (map snd (snd args))) |
|
98 |
else (); |
|
76986 | 99 |
in cite_command ctxt get_kind (args, "") end; |
76985 | 100 |
|
77017 | 101 |
val cite_keywords = |
102 |
Thy_Header.bootstrap_keywords |
|
103 |
|> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]); |
|
104 |
||
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
105 |
fun cite_command_embedded ctxt get_kind input = |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
106 |
let |
76986 | 107 |
val parser = |
108 |
Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations -- |
|
77017 | 109 |
Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) ""; |
110 |
val args = Parse.read_embedded ctxt cite_keywords parser input; |
|
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
111 |
in cite_command ctxt get_kind args end; |
76959 | 112 |
|
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
113 |
fun cite_command_parser get_kind = |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
114 |
Scan.option Args.cartouche_input -- parse_citations |
76985 | 115 |
>> (fn args => fn ctxt => cite_command_old ctxt get_kind args) || |
76964
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
116 |
Parse.embedded_input |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
117 |
>> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg); |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
118 |
|
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
119 |
in |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
120 |
|
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
121 |
fun cite_antiquotation binding get_kind = |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
122 |
Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind)) |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
123 |
(fn ctxt => fn cmd => cmd ctxt); |
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
124 |
|
c044306db39f
support embedded syntax, for use with control symbols;
wenzelm
parents:
76963
diff
changeset
|
125 |
end; |
76959 | 126 |
|
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
127 |
val _ = |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
128 |
Theory.setup |
76963 | 129 |
(cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #> |
76960 | 130 |
cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #> |
131 |
cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #> |
|
132 |
cite_antiquotation \<^binding>\<open>citep\<close> (K "citep")); |
|
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
133 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
diff
changeset
|
134 |
end; |