# 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;