author | wenzelm |
Wed, 11 Nov 2020 21:00:14 +0100 | |
changeset 72574 | d892f6d66402 |
parent 72511 | 460d743010bc |
child 72612 | 878c73cdfa0d |
permissions | -rw-r--r-- |
6203 | 1 |
(* Title: Pure/Thy/present.ML |
9416 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
6203 | 3 |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
4 |
Theory presentation: HTML and PDF-LaTeX documents. |
6203 | 5 |
*) |
6 |
||
7 |
signature PRESENT = |
|
8 |
sig |
|
72310 | 9 |
val tex_path: string -> Path.T |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
10 |
val get_bibtex_entries: theory -> string list |
66037 | 11 |
val theory_qualifier: theory -> string |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
12 |
val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit |
59445 | 13 |
val finish: unit -> unit |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
14 |
val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory |
6203 | 15 |
end; |
16 |
||
7685 | 17 |
structure Present: PRESENT = |
18 |
struct |
|
19 |
||
7727 | 20 |
|
21 |
(** paths **) |
|
22 |
||
23 |
val tex_ext = Path.ext "tex"; |
|
24 |
val tex_path = tex_ext o Path.basic; |
|
25 |
val html_ext = Path.ext "html"; |
|
26 |
val html_path = html_ext o Path.basic; |
|
27 |
val index_path = Path.basic "index.html"; |
|
11856 | 28 |
val readme_html_path = Path.basic "README.html"; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
29 |
val session_graph_path = Path.basic "session_graph.pdf"; |
72310 | 30 |
val document_path = Path.ext "pdf" o Path.basic; |
7727 | 31 |
|
62550 | 32 |
fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); |
11856 | 33 |
|
7727 | 34 |
|
14922 | 35 |
|
72047
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
36 |
(** theory data **) |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
37 |
|
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
38 |
type browser_info = {chapter: string, name: string, bibtex_entries: string list}; |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
39 |
val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}; |
7727 | 40 |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
41 |
structure Browser_Info = Theory_Data |
22846 | 42 |
( |
72047
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
43 |
type T = browser_info |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
44 |
val empty = empty_browser_info; |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
45 |
val extend = I; |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
46 |
val merge = #1; |
22846 | 47 |
); |
7727 | 48 |
|
72047
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
49 |
fun reset_browser_info thy = |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
50 |
if Browser_Info.get thy = empty_browser_info then NONE |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
51 |
else SOME (Browser_Info.put empty_browser_info thy); |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
52 |
|
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
53 |
val _ = |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
54 |
Theory.setup |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
55 |
(Theory.at_begin reset_browser_info #> |
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
56 |
Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []}); |
51567
a86c5e02ba58
proper default browser info for interactive mode, notably thy_deps;
wenzelm
parents:
51419
diff
changeset
|
57 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
58 |
val get_bibtex_entries = #bibtex_entries o Browser_Info.get; |
7727 | 59 |
|
60 |
||
72047
b9e9ff3a1e1c
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71611
diff
changeset
|
61 |
|
7727 | 62 |
(** global browser info state **) |
63 |
||
64 |
(* type browser_info *) |
|
65 |
||
54455
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
66 |
type browser_info = |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
67 |
{html_theories: string Symtab.table, |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
68 |
html_index: (int * string) list}; |
7727 | 69 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
70 |
fun make_browser_info (html_theories, html_index) : browser_info = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
71 |
{html_theories = html_theories, html_index = html_index}; |
7727 | 72 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
73 |
val empty_browser_info = make_browser_info (Symtab.empty, []); |
7727 | 74 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
75 |
fun map_browser_info f {html_theories, html_index} = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
76 |
make_browser_info (f (html_theories, html_index)); |
7727 | 77 |
|
78 |
||
79 |
(* state *) |
|
80 |
||
59173 | 81 |
val browser_info = Synchronized.var "browser_info" empty_browser_info; |
82 |
fun change_browser_info f = Synchronized.change browser_info (map_browser_info f); |
|
7727 | 83 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
84 |
fun update_html name html = change_browser_info (apfst (Symtab.update (name, html))); |
7727 | 85 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
86 |
fun add_html_index txt = change_browser_info (apsnd (cons txt)); |
7727 | 87 |
|
88 |
||
89 |
||
90 |
(** global session state **) |
|
91 |
||
92 |
(* session_info *) |
|
93 |
||
94 |
type session_info = |
|
61381 | 95 |
{symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool, |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
96 |
verbose: bool, readme: Path.T option}; |
7727 | 97 |
|
9416 | 98 |
fun make_session_info |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
99 |
(symbols, name, chapter, info_path, info, verbose, readme) = |
61381 | 100 |
{symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info, |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
101 |
verbose = verbose, readme = readme}: session_info; |
7685 | 102 |
|
103 |
||
7727 | 104 |
(* state *) |
105 |
||
32738 | 106 |
val session_info = Unsynchronized.ref (NONE: session_info option); |
7727 | 107 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
108 |
fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); |
7727 | 109 |
|
66037 | 110 |
val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name; |
111 |
||
65505 | 112 |
fun is_session_theory thy = |
113 |
(case ! session_info of |
|
114 |
NONE => false |
|
66037 | 115 |
| SOME {name, ...} => name = theory_qualifier thy); |
7727 | 116 |
|
117 |
||
14922 | 118 |
(** document preparation **) |
7727 | 119 |
|
120 |
(* init session *) |
|
121 |
||
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
122 |
fun init symbols info info_path documents (chapter, name) verbose = |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
123 |
let |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
124 |
val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; |
7727 | 125 |
|
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
126 |
val docs = |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
127 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
128 |
map (fn name => (Url.File (document_path name), name)) documents; |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
129 |
in |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
130 |
session_info := |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
131 |
SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme)); |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
132 |
Synchronized.change browser_info (K empty_browser_info); |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
133 |
add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
68511
diff
changeset
|
134 |
end; |
7727 | 135 |
|
136 |
||
11856 | 137 |
(* finish session -- output all generated text *) |
138 |
||
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58870
diff
changeset
|
139 |
fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
140 |
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
141 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
142 |
fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} => |
7727 | 143 |
let |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
144 |
val {html_theories, html_index} = Synchronized.value browser_info; |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
145 |
|
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72375
diff
changeset
|
146 |
val session_prefix = info_path + Path.basic chapter + Path.basic name; |
7727 | 147 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
148 |
fun finish_html (a, html) = File.write (session_prefix + html_path a) html; |
11856 | 149 |
|
42007 | 150 |
val _ = |
151 |
if info then |
|
72375 | 152 |
(Isabelle_System.make_directory session_prefix; |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72375
diff
changeset
|
153 |
File.write_buffer (session_prefix + index_path) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
154 |
(index_buffer html_index |> Buffer.add HTML.end_document); |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56531
diff
changeset
|
155 |
(case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
156 |
Symtab.fold (K o finish_html) html_theories (); |
54455
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
157 |
if verbose |
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
158 |
then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") |
42007 | 159 |
else ()) |
160 |
else (); |
|
7727 | 161 |
in |
59173 | 162 |
Synchronized.change browser_info (K empty_browser_info); |
15531 | 163 |
session_info := NONE |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
164 |
end); |
7727 | 165 |
|
166 |
||
167 |
(* theory elements *) |
|
168 |
||
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
169 |
fun theory_link (curr_chapter, curr_session) thy = |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
170 |
let |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
171 |
val {chapter, name = session, ...} = Browser_Info.get thy; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
172 |
val link = html_path (Context.theory_name thy); |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
173 |
in |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
174 |
if curr_session = session then SOME link |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
175 |
else if curr_chapter = chapter then |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72375
diff
changeset
|
176 |
SOME (Path.parent + Path.basic session + link) |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
177 |
else if chapter = Context.PureN then NONE |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72375
diff
changeset
|
178 |
else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
179 |
end; |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
180 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
181 |
fun begin_theory bibtex_entries update_time mk_text thy = |
61381 | 182 |
with_session_info thy (fn {symbols, name = session_name, chapter, ...} => |
54456 | 183 |
let |
184 |
val name = Context.theory_name thy; |
|
185 |
||
65505 | 186 |
val parent_specs = |
187 |
Theory.parents_of thy |> map (fn parent => |
|
188 |
(Option.map Url.File (theory_link (chapter, session_name) parent), |
|
189 |
(Context.theory_name parent))); |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
190 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
191 |
val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ())); |
65505 | 192 |
|
67302 | 193 |
val bibtex_entries' = |
65505 | 194 |
if is_session_theory thy then |
195 |
(add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)); |
|
67302 | 196 |
bibtex_entries) |
197 |
else []; |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
198 |
in |
67302 | 199 |
thy |
200 |
|> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'} |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
201 |
end); |
7727 | 202 |
|
7685 | 203 |
end; |