# HG changeset patch
# User wenzelm
# Date 1258217369 -3600
# Node ID 0c5d1485dea796f091c40fae287f20e5d4ce5f61
# Parent  cddea85bc87b8829ad32b2cff9c7fd9df2080779
isabelle_document: more explicit error output, notably for drafts;

diff -r cddea85bc87b -r 0c5d1485dea7 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Nov 13 16:10:04 2009 -0800
+++ b/src/Pure/Thy/present.ML	Sat Nov 14 17:49:29 2009 +0100
@@ -325,16 +325,16 @@
 fun isabelle_document verbose format name tags path result_path =
   let
     val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
-      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
-      " 2>&1" ^ (if verbose then "" else " >/dev/null");
+      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));
-  in
-    if verbose then writeln s else ();
-    system s;
-    File.exists doc_path orelse
-      error ("No document: " ^ quote (show_path doc_path));
-    doc_path
-  end;
+    val _ = if verbose then writeln s else ();
+    val (out, rc) = system_out s;
+    val _ =
+      if not (File.exists doc_path) orelse rc <> 0 then
+        cat_error out ("Failed to build document " ^ quote (show_path doc_path))
+      else if verbose then writeln out
+      else ();
+  in doc_path end;
 
 fun isabelle_browser graph =
   let