# HG changeset patch
# User wenzelm
# Date 939836495 -7200
# Node ID a4acf1b4d5a8d8ed43e790203b2a53a5621aa50c
# Parent  d28dff7ac48dcde9e65026731698cc38d3e3604a
system;

diff -r d28dff7ac48d -r a4acf1b4d5a8 src/Pure/Thy/present.ML
--- 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, ...} =>
diff -r d28dff7ac48d -r a4acf1b4d5a8 src/Pure/Thy/thm_deps.ML
--- 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;