1.1 --- a/src/Pure/Thy/present.ML	Fri Jun 18 00:32:54 2004 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Jun 18 20:07:31 2004 +0200
     1.3 @@ -323,13 +323,13 @@
     1.4    write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
     1.5  
     1.6  
     1.7 -fun isatool_document doc_format path =
     1.8 +fun isatool_document verbose doc_format path =
     1.9    let
    1.10      val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
    1.11 -      File.quote_sysify_path path ^ " 2>&1";
    1.12 +      File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
    1.13    in
    1.14 -    writeln s;
    1.15 -    writeln (Output.raw (execute s));
    1.16 +    if verbose then writeln s else ();
    1.17 +    system s;
    1.18      if File.exists (Path.ext doc_format path) then ()
    1.19      else error "Failed to build document"
    1.20    end;
    1.21 @@ -398,7 +398,7 @@
    1.22  
    1.23      (case doc_prefix1 of None => () | Some path =>
    1.24       (prepare_sources path;
    1.25 -      isatool_document doc_format path;
    1.26 +      isatool_document true doc_format path;
    1.27        conditional verbose (fn () =>
    1.28          std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n"))));
    1.29  
    1.30 @@ -527,7 +527,7 @@
    1.31        |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
    1.32        |> File.write (Path.append doc_path (tex_path name)));
    1.33      val _ = write_tex_index tex_index doc_path;
    1.34 -    val _ = isatool_document doc_format doc_path;
    1.35 +    val _ = isatool_document false doc_format doc_path;
    1.36    in Path.ext doc_format doc_path end;
    1.37  
    1.38