327 (fn {name, html_prefix, doc_prefix, graph_path, all_graph_path, path, ...} => |
327 (fn {name, html_prefix, doc_prefix, graph_path, all_graph_path, path, ...} => |
328 let |
328 let |
329 val {theories, tex_index, html_index, graph, all_graph} = ! browser_info; |
329 val {theories, tex_index, html_index, graph, all_graph} = ! browser_info; |
330 |
330 |
331 fun finish_node (a, {tex_source, html_source = _, html}) = |
331 fun finish_node (a, {tex_source, html_source = _, html}) = |
332 (apsome (fn p => Buffer.write_nonempty (Path.append p (tex_path a)) tex_source) doc_prefix; |
332 (apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source) doc_prefix; |
333 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html)); |
333 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html)); |
334 in |
334 in |
335 seq finish_node (Symtab.dest theories); |
335 seq finish_node (Symtab.dest theories); |
336 Buffer.write (Path.append html_prefix pre_index_path) html_index; |
336 Buffer.write (Path.append html_prefix pre_index_path) html_index; |
337 apsome (fn p => Buffer.write (Path.append p doc_index_path) tex_index) doc_prefix; |
337 apsome (fn p => Buffer.write (Path.append p doc_index_path) tex_index) doc_prefix; |