311 if verbose |
311 if verbose |
312 then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") |
312 then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") |
313 else ()) |
313 else ()) |
314 else (); |
314 else (); |
315 |
315 |
316 fun prepare_sources doc_copy doc_dir = |
|
317 (Isabelle_System.mkdirs doc_dir; |
|
318 if doc_copy then Isabelle_System.copy_dir document_path doc_dir else (); |
|
319 Isabelle_System.isabelle_tool "latex" |
|
320 ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); |
|
321 (case opt_graphs of NONE => () | SOME (pdf, eps) => |
|
322 (File.write (Path.append doc_dir graph_pdf_path) pdf; |
|
323 File.write (Path.append doc_dir graph_eps_path) eps)); |
|
324 write_tex_index tex_index doc_dir; |
|
325 List.app (fn (a, {tex_source, ...}) => |
|
326 write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys); |
|
327 |
|
328 fun document_job doc_prefix backdrop (name, tags) = |
316 fun document_job doc_prefix backdrop (name, tags) = |
329 let |
317 let |
330 val _ = |
318 val _ = |
331 File.eq (document_path, doc_prefix) andalso |
319 File.eq (document_path, doc_prefix) andalso |
332 error ("Overlap of document input and output directory " ^ Path.print doc_prefix); |
320 error ("Overlap of document input and output directory " ^ Path.print doc_prefix); |
333 val dir = Path.append doc_prefix (Path.basic name); |
321 val doc_dir = Path.append doc_prefix (Path.basic name); |
334 val copy = not (File.eq (document_path, dir)); |
322 val _ = Isabelle_System.mkdirs doc_dir; |
335 val _ = prepare_sources copy dir; |
323 val _ = |
336 fun inform doc = |
324 if File.eq (document_path, doc_dir) then () |
337 if verbose orelse not backdrop then |
325 else Isabelle_System.copy_dir document_path doc_dir; |
338 Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") |
326 val _ = |
339 else (); |
327 Isabelle_System.isabelle_tool "latex" |
|
328 ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); |
|
329 val _ = |
|
330 (case opt_graphs of |
|
331 NONE => () |
|
332 | SOME (pdf, eps) => |
|
333 (File.write (Path.append doc_dir graph_pdf_path) pdf; |
|
334 File.write (Path.append doc_dir graph_eps_path) eps)); |
|
335 val _ = write_tex_index tex_index doc_dir; |
|
336 val _ = |
|
337 List.app (fn (a, {tex_source, ...}) => |
|
338 write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys; |
340 in |
339 in |
341 fn () => |
340 fn () => |
342 (isabelle_document {verbose = true, purge = backdrop} doc_format name tags dir, inform) |
341 (isabelle_document {verbose = true, purge = backdrop} doc_format name tags doc_dir, |
|
342 fn doc => |
|
343 if verbose orelse not backdrop then |
|
344 Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") |
|
345 else ()) |
343 end; |
346 end; |
344 |
347 |
345 val jobs = |
348 val jobs = |
346 (if info orelse is_none doc_output then |
349 (if info orelse is_none doc_output then |
347 map (document_job session_prefix true) documents |
350 map (document_job session_prefix true) documents |