16 val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
16 val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
17 path: string, parents: string list} list -> Path.T -> unit |
17 path: string, parents: string list} list -> Path.T -> unit |
18 val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
18 val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
19 path: string, parents: string list} list -> unit |
19 path: string, parents: string list} list -> unit |
20 val init: bool -> bool -> string -> string -> bool -> string list -> string list -> |
20 val init: bool -> bool -> string -> string -> bool -> string list -> string list -> |
21 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> |
21 string -> string * string -> Url.T option * bool -> bool -> |
22 theory list -> unit (*not thread-safe!*) |
22 theory list -> unit (*not thread-safe!*) |
23 val finish: unit -> unit (*not thread-safe!*) |
23 val finish: unit -> unit (*not thread-safe!*) |
24 val init_theory: string -> unit |
24 val init_theory: string -> unit |
25 val theory_source: string -> (unit -> HTML.text) -> unit |
25 val theory_source: string -> (unit -> HTML.text) -> unit |
26 val theory_output: string -> string -> unit |
26 val theory_output: string -> string -> unit |
208 (* session_info *) |
208 (* session_info *) |
209 |
209 |
210 type session_info = |
210 type session_info = |
211 {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, |
211 {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, |
212 info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, |
212 info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, |
213 dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool, |
213 doc_dump: (string * string), remote_path: Url.T option, verbose: bool, |
214 readme: Path.T option}; |
214 readme: Path.T option}; |
215 |
215 |
216 fun make_session_info |
216 fun make_session_info |
217 (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, |
217 (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, |
218 dump_prefix, remote_path, verbose, readme) = |
218 doc_dump, remote_path, verbose, readme) = |
219 {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, |
219 {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, |
220 info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, |
220 info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, |
221 dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose, |
221 doc_dump = doc_dump, remote_path = remote_path, verbose = verbose, |
222 readme = readme}: session_info; |
222 readme = readme}: session_info; |
223 |
223 |
224 |
224 |
225 (* state *) |
225 (* state *) |
226 |
226 |
271 |
271 |
272 (* init session *) |
272 (* init session *) |
273 |
273 |
274 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
274 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
275 |
275 |
276 fun init build info info_path doc doc_graph doc_variants path name dump_prefix |
276 fun init build info info_path doc doc_graph doc_variants path name |
277 (remote_path, first_time) verbose thys = |
277 (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys = |
278 if not build andalso not info andalso doc = "" andalso is_none dump_prefix then |
278 if not build andalso not info andalso doc = "" andalso dump_prefix = "" then |
279 (browser_info := empty_browser_info; session_info := NONE) |
279 (browser_info := empty_browser_info; session_info := NONE) |
280 else |
280 else |
281 let |
281 let |
282 val parent_name = name_of_session (take (length path - 1) path); |
282 val parent_name = name_of_session (take (length path - 1) path); |
283 val session_name = name_of_session path; |
283 val session_name = name_of_session path; |
307 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
307 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
308 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
308 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
309 in |
309 in |
310 session_info := |
310 session_info := |
311 SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
311 SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
312 info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme)); |
312 info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme)); |
313 browser_info := init_browser_info remote_path path thys; |
313 browser_info := init_browser_info remote_path path thys; |
314 add_html_index (0, index_text) |
314 add_html_index (0, index_text) |
315 end; |
315 end; |
316 |
316 |
317 |
317 |
358 write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; |
358 write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; |
359 |
359 |
360 |
360 |
361 fun finish () = |
361 fun finish () = |
362 session_default () (fn {name, info, html_prefix, doc_format, |
362 session_default () (fn {name, info, html_prefix, doc_format, |
363 doc_graph, documents, dump_prefix, path, verbose, readme, ...} => |
363 doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} => |
364 let |
364 let |
365 val {theories, files, tex_index, html_index, graph} = ! browser_info; |
365 val {theories, files, tex_index, html_index, graph} = ! browser_info; |
366 val thys = Symtab.dest theories; |
366 val thys = Symtab.dest theories; |
367 val parent_html_prefix = Path.append html_prefix Path.parent; |
367 val parent_html_prefix = Path.append html_prefix Path.parent; |
368 |
368 |
369 fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path; |
|
370 fun finish_html (a, {html, ...}: theory_info) = |
369 fun finish_html (a, {html, ...}: theory_info) = |
371 File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); |
370 File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); |
372 |
371 |
373 val sorted_graph = sorted_index graph; |
372 val sorted_graph = sorted_index graph; |
374 val opt_graphs = |
373 val opt_graphs = |
375 if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then |
374 if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then |
376 SOME (isabelle_browser sorted_graph) |
375 SOME (isabelle_browser sorted_graph) |
377 else NONE; |
376 else NONE; |
378 |
377 |
379 fun prepare_sources cp path = |
378 fun prepare_sources doc_dir doc_mode = |
380 (Isabelle_System.mkdirs path; |
379 (Isabelle_System.mkdirs doc_dir; |
381 if cp then Isabelle_System.copy_dir document_path path else (); |
380 if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir |
382 Isabelle_System.isabelle_tool "latex" |
381 else if doc_mode = "tex+sty" then |
383 ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex"))); |
382 ignore (Isabelle_System.isabelle_tool "latex" |
|
383 ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")))) |
|
384 else if doc_mode = "tex" then () |
|
385 else error ("Illegal document dump mode: " ^ quote doc_mode); |
384 (case opt_graphs of NONE => () | SOME (pdf, eps) => |
386 (case opt_graphs of NONE => () | SOME (pdf, eps) => |
385 (File.write (Path.append path graph_pdf_path) pdf; |
387 (File.write (Path.append doc_dir graph_pdf_path) pdf; |
386 File.write (Path.append path graph_eps_path) eps)); |
388 File.write (Path.append doc_dir graph_eps_path) eps)); |
387 write_tex_index tex_index path; |
389 write_tex_index tex_index doc_dir; |
388 List.app (finish_tex path) thys); |
390 List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys); |
389 val _ = |
391 val _ = |
390 if info then |
392 if info then |
391 (Isabelle_System.mkdirs (Path.append html_prefix session_path); |
393 (Isabelle_System.mkdirs (Path.append html_prefix session_path); |
392 File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); |
394 File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); |
393 File.write (Path.append html_prefix session_entries_path) ""; |
395 File.write (Path.append html_prefix session_entries_path) ""; |
405 if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") |
407 if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") |
406 else ()) |
408 else ()) |
407 else (); |
409 else (); |
408 |
410 |
409 val _ = |
411 val _ = |
410 (case dump_prefix of NONE => () | SOME (cp, path) => |
412 if dump_prefix = "" then () |
411 (prepare_sources cp path; |
413 else |
412 if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") |
414 let |
413 else ())); |
415 val path = Path.explode dump_prefix; |
|
416 val _ = prepare_sources path dump_mode; |
|
417 in |
|
418 if verbose then |
|
419 Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") |
|
420 else () |
|
421 end; |
414 |
422 |
415 val doc_paths = |
423 val doc_paths = |
416 documents |> Par_List.map (fn (name, tags) => |
424 documents |> Par_List.map (fn (name, tags) => |
417 let |
425 let |
418 val path = Path.append html_prefix (Path.basic name); |
426 val path = Path.append html_prefix (Path.basic name); |
419 val _ = prepare_sources true path; |
427 val _ = prepare_sources path "all"; |
420 in isabelle_document true doc_format name tags path html_prefix end); |
428 in isabelle_document true doc_format name tags path html_prefix end); |
421 val _ = |
429 val _ = |
422 if verbose then |
430 if verbose then |
423 doc_paths |
431 doc_paths |
424 |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")) |
432 |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")) |