isatool_document: writeln output;
authorwenzelm
Wed, 16 Jun 2004 20:42:22 +0200
changeset 14958 801178863f17
parent 14957 0e94a1ccc6ae
child 14959 014d4e006739
isatool_document: writeln output;
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;