# HG changeset patch
# User wenzelm
# Date 1513082051 -3600
# Node ID 3457d7d43ee95e89f16540ce615489fe001b4d3e
# Parent  a58bbe66ac812857c503175d2309b026fb1af133
tuned message;

diff -r a58bbe66ac81 -r 3457d7d43ee9 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Dec 12 12:35:01 2017 +0100
+++ b/src/Pure/Thy/present.ML	Tue Dec 12 13:34:11 2017 +0100
@@ -197,10 +197,7 @@
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
-    val _ =
-      if not (File.exists doc_path) orelse rc <> 0 then
-        cat_error (trim_line err) ("Failed to build document " ^ quote (show_path doc_path))
-      else ();
+    val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
     val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   in doc_path end;
 
diff -r a58bbe66ac81 -r 3457d7d43ee9 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Tue Dec 12 12:35:01 2017 +0100
+++ b/src/Pure/Thy/present.scala	Tue Dec 12 13:34:11 2017 +0100
@@ -209,7 +209,7 @@
 
     if (!result.ok) {
       cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
-        "Failed to build document in directory " + File.path(dir.absolute_file))
+        "Failed to build document in " + File.path(dir.absolute_file))
     }
 
     bash("[ -f " + root_bash(document_format) + " ] && cp -f " +