src/Pure/Thy/present.ML

 
 
 (* finish session *)
 
 fun isatool_document doc_format doc_prefix =
-  let val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
-  in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
+  let
+    val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'";
+  in
+    writeln cmd;
+    if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then
+      error "Failed to build document"
+    else ()
+  end;
 
 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
 
 fun write_texes src name (path, None) = write_tex src name path
   | write_texes src name (path, Some path') = (write_tex src name path; write_tex src name path');