--- a/src/Pure/Thy/present.ML Wed Oct 13 19:41:18 1999 +0200
+++ b/src/Pure/Thy/present.ML Wed Oct 13 19:41:35 1999 +0200
@@ -326,7 +326,7 @@
fun isatool_document doc_format doc_prefix =
let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
- in writeln cmd; writeln (execute cmd) end;
+ in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
fun finish () = with_session ()
(fn {name, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, path, ...} =>
--- a/src/Pure/Thy/thm_deps.ML Wed Oct 13 19:41:18 1999 +0200
+++ b/src/Pure/Thy/thm_deps.ML Wed Oct 13 19:41:35 1999 +0200
@@ -75,7 +75,7 @@
map (#der o rep_thm) thms))));
val path = File.tmp_path (Path.unpack "theorems.graph");
val _ = put_graph gra path;
- val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
+ val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
in () end;
end;