290 val sess_prefix = Path.make path; |
290 val sess_prefix = Path.make path; |
291 val html_prefix = Path.append (Path.expand output_path) sess_prefix; |
291 val html_prefix = Path.append (Path.expand output_path) sess_prefix; |
292 |
292 |
293 val (doc_prefix1, documents) = |
293 val (doc_prefix1, documents) = |
294 if doc = "" then (NONE, []) |
294 if doc = "" then (NONE, []) |
295 else if not (File.exists document_path) then |
295 else if not (can File.check_dir document_path) then |
296 (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); |
296 (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); |
297 (NONE, [])) |
297 (NONE, [])) |
298 else (SOME (Path.append html_prefix document_path, html_prefix), |
298 else (SOME (Path.append html_prefix document_path, html_prefix), |
299 read_variants doc_variants); |
299 read_variants doc_variants); |
300 |
300 |
312 map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
312 map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
313 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
313 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
314 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
314 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
315 in |
315 in |
316 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
316 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
317 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
317 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
318 browser_info := init_browser_info remote_path path thys; |
318 browser_info := init_browser_info remote_path path thys; |
319 add_html_index (0, index_text) |
319 add_html_index (0, index_text) |
320 end); |
320 end); |
321 |
321 |
322 |
322 |