isatool document: check output file (workaround PolyML problem with RC);

--- a/src/Pure/Thy/present.ML	Fri Mar 31 22:39:39 2000 +0200
+++ b/src/Pure/Thy/present.ML	Sat Apr 01 20:09:20 2000 +0200
@@ -327,8 +327,14 @@
 (* 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;