equal
deleted
inserted
replaced
325 |
325 |
326 |
326 |
327 (* finish session *) |
327 (* finish session *) |
328 |
328 |
329 fun isatool_document doc_format doc_prefix = |
329 fun isatool_document doc_format doc_prefix = |
330 let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'" |
330 let val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'" |
331 in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end; |
331 in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end; |
332 |
332 |
333 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src; |
333 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src; |
334 |
334 |
335 fun write_texes src name (path, None) = write_tex src name path |
335 fun write_texes src name (path, None) = write_tex src name path |