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