author | wenzelm |
Fri, 29 Dec 2017 21:17:43 +0100 | |
changeset 67302 | 48ca44fdc038 |
parent 67297 | 86a099f896fc |
child 67420 | c4c8787ed669 |
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 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
9 |
val get_bibtex_entries: theory -> string list |
66037 | 10 |
val theory_qualifier: theory -> string |
56614 | 11 |
val document_enabled: string -> bool |
56612 | 12 |
val document_variants: string -> (string * string) list |
61381 | 13 |
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
14 |
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit |
59445 | 15 |
val finish: unit -> unit |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
16 |
val theory_output: Position.T -> theory -> Latex.text list -> unit |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
17 |
val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory |
6203 | 18 |
end; |
19 |
||
7685 | 20 |
structure Present: PRESENT = |
21 |
struct |
|
22 |
||
7727 | 23 |
|
24 |
(** paths **) |
|
25 |
||
26 |
val tex_ext = Path.ext "tex"; |
|
27 |
val tex_path = tex_ext o Path.basic; |
|
28 |
val html_ext = Path.ext "html"; |
|
29 |
val html_path = html_ext o Path.basic; |
|
30 |
val index_path = Path.basic "index.html"; |
|
11856 | 31 |
val readme_html_path = Path.basic "README.html"; |
8196 | 32 |
val doc_indexN = "session"; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
33 |
val session_graph_path = Path.basic "session_graph.pdf"; |
7727 | 34 |
|
62550 | 35 |
fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); |
11856 | 36 |
|
7727 | 37 |
|
14922 | 38 |
|
7727 | 39 |
(** additional theory data **) |
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 |
( |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
43 |
type T = {chapter: string, name: string, bibtex_entries: string list}; |
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
44 |
val empty = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}: T; |
16503 | 45 |
fun extend _ = empty; |
33522 | 46 |
fun merge _ = empty; |
22846 | 47 |
); |
7727 | 48 |
|
53171 | 49 |
val _ = Theory.setup |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
50 |
(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
|
51 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
52 |
val get_bibtex_entries = #bibtex_entries o Browser_Info.get; |
7727 | 53 |
|
54 |
||
55 |
(** global browser info state **) |
|
56 |
||
57 |
(* type theory_info *) |
|
58 |
||
54456 | 59 |
type theory_info = {tex_source: string, html_source: string}; |
7727 | 60 |
|
54456 | 61 |
fun make_theory_info (tex_source, html_source) = |
62 |
{tex_source = tex_source, html_source = html_source}: theory_info; |
|
7727 | 63 |
|
54456 | 64 |
fun map_theory_info f {tex_source, html_source} = |
65 |
make_theory_info (f (tex_source, html_source)); |
|
7727 | 66 |
|
67 |
||
68 |
(* type browser_info *) |
|
69 |
||
54455
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
70 |
type browser_info = |
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
71 |
{theories: theory_info Symtab.table, |
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
72 |
tex_index: (int * string) list, |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
73 |
html_index: (int * string) list}; |
7727 | 74 |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
75 |
fun make_browser_info (theories, tex_index, html_index) : browser_info = |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
76 |
{theories = theories, tex_index = tex_index, html_index = html_index}; |
7727 | 77 |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
78 |
val empty_browser_info = make_browser_info (Symtab.empty, [], []); |
7727 | 79 |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
80 |
fun map_browser_info f {theories, tex_index, html_index} = |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
81 |
make_browser_info (f (theories, tex_index, html_index)); |
7727 | 82 |
|
83 |
||
84 |
(* state *) |
|
85 |
||
59173 | 86 |
val browser_info = Synchronized.var "browser_info" empty_browser_info; |
87 |
fun change_browser_info f = Synchronized.change browser_info (map_browser_info f); |
|
7727 | 88 |
|
89 |
fun init_theory_info name info = |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
90 |
change_browser_info (fn (theories, tex_index, html_index) => |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
91 |
(Symtab.update (name, info) theories, tex_index, html_index)); |
7727 | 92 |
|
93 |
fun change_theory_info name f = |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
94 |
change_browser_info (fn (theories, tex_index, html_index) => |
17412 | 95 |
(case Symtab.lookup theories name of |
27491
c8178a6a6480
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
wenzelm
parents:
27329
diff
changeset
|
96 |
NONE => error ("Browser info: cannot access theory document " ^ quote name) |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
97 |
| SOME info => (Symtab.update (name, map_theory_info f info) theories, tex_index, html_index))); |
7727 | 98 |
|
99 |
||
100 |
fun add_tex_index txt = |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
101 |
change_browser_info (fn (theories, tex_index, html_index) => |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
102 |
(theories, txt :: tex_index, html_index)); |
7727 | 103 |
|
104 |
fun add_html_index txt = |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
105 |
change_browser_info (fn (theories, tex_index, html_index) => |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
106 |
(theories, tex_index, txt :: html_index)); |
7727 | 107 |
|
108 |
||
109 |
||
110 |
(** global session state **) |
|
111 |
||
112 |
(* session_info *) |
|
113 |
||
114 |
type session_info = |
|
61381 | 115 |
{symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool, |
116 |
doc_format: string, doc_output: Path.T option, doc_files: (Path.T * Path.T) list, |
|
117 |
graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option}; |
|
7727 | 118 |
|
9416 | 119 |
fun make_session_info |
61381 | 120 |
(symbols, name, chapter, info_path, info, doc_format, doc_output, doc_files, |
59446 | 121 |
graph_file, documents, verbose, readme) = |
61381 | 122 |
{symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info, |
123 |
doc_format = doc_format, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file, |
|
59446 | 124 |
documents = documents, verbose = verbose, readme = readme}: session_info; |
7685 | 125 |
|
126 |
||
7727 | 127 |
(* state *) |
128 |
||
32738 | 129 |
val session_info = Unsynchronized.ref (NONE: session_info option); |
7727 | 130 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
131 |
fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); |
7727 | 132 |
|
66037 | 133 |
val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name; |
134 |
||
65505 | 135 |
fun is_session_theory thy = |
136 |
(case ! session_info of |
|
137 |
NONE => false |
|
66037 | 138 |
| SOME {name, ...} => name = theory_qualifier thy); |
7727 | 139 |
|
140 |
||
14922 | 141 |
(** document preparation **) |
7727 | 142 |
|
56614 | 143 |
(* options *) |
144 |
||
145 |
fun document_enabled s = s <> "" andalso s <> "false"; |
|
17082 | 146 |
|
56612 | 147 |
fun document_variants str = |
148 |
let |
|
149 |
fun read_variant s = |
|
150 |
(case space_explode "=" s of |
|
151 |
[name] => (name, "") |
|
152 |
| [name, tags] => (name, tags) |
|
153 |
| _ => error ("Malformed document variant specification: " ^ quote s)); |
|
154 |
val variants = map read_variant (space_explode ":" str); |
|
155 |
val _ = |
|
156 |
(case duplicates (op =) (map #1 variants) of |
|
157 |
[] => () |
|
158 |
| dups => error ("Duplicate document variants: " ^ commas_quote dups)); |
|
159 |
in variants end; |
|
17082 | 160 |
|
161 |
||
7727 | 162 |
(* init session *) |
163 |
||
61381 | 164 |
fun init symbols build info info_path doc document_output doc_variants doc_files graph_file |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
165 |
(chapter, name) verbose = |
56530
5c178501cf78
removed obsolete doc_dump option (see also 892061142ba6);
wenzelm
parents:
54683
diff
changeset
|
166 |
if not build andalso not info andalso doc = "" then |
59173 | 167 |
(Synchronized.change browser_info (K empty_browser_info); session_info := NONE) |
11856 | 168 |
else |
169 |
let |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
170 |
val doc_output = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
171 |
if document_output = "" then NONE else SOME (Path.explode document_output); |
7727 | 172 |
|
66945
b6f787a17fbe
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
wenzelm
parents:
66680
diff
changeset
|
173 |
val documents = if doc = "" orelse null doc_files then [] else doc_variants; |
51419
5313abe76bd4
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
wenzelm
parents:
51415
diff
changeset
|
174 |
val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; |
7727 | 175 |
|
17082 | 176 |
val docs = |
177 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
|
42007 | 178 |
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
11856 | 179 |
in |
42007 | 180 |
session_info := |
61381 | 181 |
SOME (make_session_info (symbols, name, chapter, info_path, info, doc, |
59446 | 182 |
doc_output, doc_files, graph_file, documents, verbose, readme)); |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
183 |
Synchronized.change browser_info (K empty_browser_info); |
61381 | 184 |
add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
185 |
end; |
7727 | 186 |
|
187 |
||
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28375
diff
changeset
|
188 |
(* isabelle tool wrappers *) |
17082 | 189 |
|
67197 | 190 |
fun isabelle_document {verbose} format name tags dir = |
17082 | 191 |
let |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67175
diff
changeset
|
192 |
val script = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67175
diff
changeset
|
193 |
"isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67175
diff
changeset
|
194 |
" -n " ^ Bash.string name ^ " -t " ^ Bash.string tags; |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
195 |
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format]; |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67175
diff
changeset
|
196 |
val _ = if verbose then writeln script else (); |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67175
diff
changeset
|
197 |
val {out, err, rc, ...} = Bash.process script; |
67180 | 198 |
val _ = if verbose then writeln (trim_line (normalize_lines out)) else (); |
67187 | 199 |
val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else (); |
33682
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
200 |
in doc_path end; |
17082 | 201 |
|
202 |
||
11856 | 203 |
(* finish session -- output all generated text *) |
204 |
||
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58870
diff
changeset
|
205 |
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
|
206 |
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
|
207 |
|
14922 | 208 |
fun write_tex src name path = |
28027 | 209 |
File.write_buffer (Path.append path (tex_path name)) src; |
14922 | 210 |
|
211 |
fun write_tex_index tex_index path = |
|
67175 | 212 |
write_tex (index_buffer tex_index) doc_indexN path; |
14922 | 213 |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
214 |
fun finish () = |
59446 | 215 |
with_session_info () (fn {name, chapter, info, info_path, doc_format, |
59445 | 216 |
doc_output, doc_files, graph_file, documents, verbose, readme, ...} => |
7727 | 217 |
let |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
218 |
val {theories, tex_index, html_index} = Synchronized.value browser_info; |
11856 | 219 |
val thys = Symtab.dest theories; |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
220 |
|
61372 | 221 |
val session_prefix = |
222 |
Path.append (Path.append info_path (Path.basic chapter)) (Path.basic name); |
|
7727 | 223 |
|
54456 | 224 |
fun finish_html (a, {html_source, ...}: theory_info) = |
225 |
File.write (Path.append session_prefix (html_path a)) html_source; |
|
11856 | 226 |
|
42007 | 227 |
val _ = |
228 |
if info then |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
229 |
(Isabelle_System.mkdirs session_prefix; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
230 |
File.write_buffer (Path.append session_prefix index_path) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
231 |
(index_buffer html_index |> Buffer.add HTML.end_document); |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56531
diff
changeset
|
232 |
(case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); |
42007 | 233 |
List.app finish_html thys; |
54455
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
234 |
if verbose |
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53171
diff
changeset
|
235 |
then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") |
42007 | 236 |
else ()) |
237 |
else (); |
|
238 |
||
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56531
diff
changeset
|
239 |
fun document_job doc_prefix backdrop (doc_name, tags) = |
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
240 |
let |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56531
diff
changeset
|
241 |
val doc_dir = Path.append doc_prefix (Path.basic doc_name); |
67197 | 242 |
fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else (); |
243 |
val _ = purge (); |
|
56531 | 244 |
val _ = Isabelle_System.mkdirs doc_dir; |
245 |
val _ = |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62589
diff
changeset
|
246 |
Isabelle_System.bash ("isabelle latex -o sty " ^ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62589
diff
changeset
|
247 |
File.bash_path (Path.append doc_dir (Path.basic "root.tex"))); |
57885 | 248 |
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
249 |
val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path); |
56531 | 250 |
val _ = write_tex_index tex_index doc_dir; |
251 |
val _ = |
|
252 |
List.app (fn (a, {tex_source, ...}) => |
|
253 |
write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys; |
|
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
254 |
in |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
255 |
fn () => |
67197 | 256 |
(isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (), |
56531 | 257 |
fn doc => |
258 |
if verbose orelse not backdrop then |
|
259 |
Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") |
|
260 |
else ()) |
|
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
261 |
end; |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
262 |
|
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
263 |
val jobs = |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
264 |
(if info orelse is_none doc_output then |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
265 |
map (document_job session_prefix true) documents |
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
266 |
else []) @ |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
267 |
(case doc_output of |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
268 |
NONE => [] |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
269 |
| SOME path => map (document_job path false) documents); |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
270 |
|
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
271 |
val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>); |
7727 | 272 |
in |
59173 | 273 |
Synchronized.change browser_info (K empty_browser_info); |
15531 | 274 |
session_info := NONE |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
275 |
end); |
7727 | 276 |
|
277 |
||
278 |
(* theory elements *) |
|
279 |
||
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
280 |
fun theory_output pos thy body = |
54458
96ccc8972fc7
prefer explicit "document" flag -- eliminated stateful Present.no_document;
wenzelm
parents:
54456
diff
changeset
|
281 |
with_session_info () (fn _ => |
65505 | 282 |
if is_session_theory thy then |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
283 |
let val name = Context.theory_name thy in |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
284 |
(change_theory_info name o apfst) |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
285 |
(fn _ => |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
286 |
let val latex = Latex.isabelle_body name body |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
287 |
in Latex.output_text latex ^ Latex.output_positions pos latex end) |
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67192
diff
changeset
|
288 |
end |
65505 | 289 |
else ()); |
7727 | 290 |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
291 |
fun theory_link (curr_chapter, curr_session) thy = |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
292 |
let |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
293 |
val {chapter, name = session, ...} = Browser_Info.get thy; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
294 |
val link = html_path (Context.theory_name thy); |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
295 |
in |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
296 |
if curr_session = session then SOME link |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
297 |
else if curr_chapter = chapter then |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
298 |
SOME (Path.appends [Path.parent, Path.basic session, link]) |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
299 |
else if chapter = Context.PureN then NONE |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
300 |
else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link]) |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
301 |
end; |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
302 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
303 |
fun begin_theory bibtex_entries update_time mk_text thy = |
61381 | 304 |
with_session_info thy (fn {symbols, name = session_name, chapter, ...} => |
54456 | 305 |
let |
306 |
val name = Context.theory_name thy; |
|
307 |
||
65505 | 308 |
val parent_specs = |
309 |
Theory.parents_of thy |> map (fn parent => |
|
310 |
(Option.map Url.File (theory_link (chapter, session_name) parent), |
|
311 |
(Context.theory_name parent))); |
|
61381 | 312 |
val html_source = HTML.theory symbols name parent_specs (mk_text ()); |
65505 | 313 |
val _ = init_theory_info name (make_theory_info ("", html_source)); |
314 |
||
67302 | 315 |
val bibtex_entries' = |
65505 | 316 |
if is_session_theory thy then |
317 |
(add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)); |
|
67302 | 318 |
add_tex_index (update_time, Latex.theory_entry name); |
319 |
bibtex_entries) |
|
320 |
else []; |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67285
diff
changeset
|
321 |
in |
67302 | 322 |
thy |
323 |
|> 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
|
324 |
end); |
7727 | 325 |
|
7685 | 326 |
end; |