# HG changeset patch
# User wenzelm
# Date 1087411342 -7200
# Node ID 801178863f17e268206cc5771b5dc47d51f7e895
# Parent  0e94a1ccc6aeb7a24f3a6fbe06845bc6f38d9cd2
isatool_document: writeln output;

diff -r 0e94a1ccc6ae -r 801178863f17 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Jun 16 20:37:29 2004 +0200
+++ b/src/Pure/Thy/present.ML	Wed Jun 16 20:42:22 2004 +0200
@@ -324,13 +324,14 @@
 
 
 fun isatool_document doc_format path =
-  let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
-    File.quote_sysify_path path ^ " 2>&1"
+  let
+    val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
+      File.quote_sysify_path path ^ " 2>&1";
   in
     writeln s;
-    if system s <> 0 orelse not (File.exists (Path.ext doc_format path)) then
-      error "Failed to build document"
-    else ()
+    writeln (Output.raw (execute s));
+    if File.exists (Path.ext doc_format path) then ()
+    else error "Failed to build document"
   end;
 
 fun isatool_browser graph =
@@ -342,8 +343,8 @@
       File.quote_sysify_path gpath;
   in
     write_graph graph gpath;
-    if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath) then
-      error "Failed to prepare dependency graph"
+    if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath)
+    then error "Failed to prepare dependency graph"
     else
       let val pdf = File.read pdfpath and eps = File.read epspath
       in File.rm pdfpath; File.rm epspath; File.rm gpath; (pdf, eps) end
@@ -535,9 +536,7 @@
 
 val setup = [BrowserInfoData.init];
 
-
 end;
 
-
 structure BasicPresent: BASIC_PRESENT = Present;
 open BasicPresent;