# HG changeset patch
# User wenzelm
# Date 1087582051 -7200
# Node ID 0343cf20d5680e90c851f76774cb89c5c7149b6c
# Parent  53e6823b0971c4525c78abdee209e7af1d5a9682
isatool_document: verbose option;

diff -r 53e6823b0971 -r 0343cf20d568 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Jun 18 00:32:54 2004 +0200
+++ b/src/Pure/Thy/present.ML	Fri Jun 18 20:07:31 2004 +0200
@@ -323,13 +323,13 @@
   write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
 
 
-fun isatool_document doc_format path =
+fun isatool_document verbose doc_format path =
   let
     val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
-      File.quote_sysify_path path ^ " 2>&1";
+      File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
   in
-    writeln s;
-    writeln (Output.raw (execute s));
+    if verbose then writeln s else ();
+    system s;
     if File.exists (Path.ext doc_format path) then ()
     else error "Failed to build document"
   end;
@@ -398,7 +398,7 @@
 
     (case doc_prefix1 of None => () | Some path =>
      (prepare_sources path;
-      isatool_document doc_format path;
+      isatool_document true doc_format path;
       conditional verbose (fn () =>
         std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n"))));
 
@@ -527,7 +527,7 @@
       |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
       |> File.write (Path.append doc_path (tex_path name)));
     val _ = write_tex_index tex_index doc_path;
-    val _ = isatool_document doc_format doc_path;
+    val _ = isatool_document false doc_format doc_path;
   in Path.ext doc_format doc_path end;