# HG changeset patch
# User wenzelm
# Date 1512935409 -3600
# Node ID dcac4659d482292d98628bad096591fccf836e16
# Parent  35a4bf0f13b3fae0233c05b84e946ad1d4ddccc8
tuned messages;

diff -r 35a4bf0f13b3 -r dcac4659d482 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Dec 10 20:31:14 2017 +0100
+++ b/src/Pure/Thy/present.ML	Sun Dec 10 20:50:09 2017 +0100
@@ -196,10 +196,10 @@
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
-    val _ = if verbose then writeln (normalize_lines out) else ();
+    val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
     val _ =
       if not (File.exists doc_path) orelse rc <> 0 then
-        cat_error err ("Failed to build document " ^ quote (show_path doc_path))
+        cat_error (trim_line err) ("Failed to build document " ^ quote (show_path doc_path))
       else ();
     val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   in doc_path end;
diff -r 35a4bf0f13b3 -r dcac4659d482 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sun Dec 10 20:31:14 2017 +0100
+++ b/src/Pure/Thy/present.scala	Sun Dec 10 20:50:09 2017 +0100
@@ -182,10 +182,7 @@
       "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
 
     def bash(script: String): Process_Result =
-    {
-      Output.writeln(script)  // FIXME
       Isabelle_System.bash(script, cwd = dir.file)
-    }
 
 
     /* prepare document */
@@ -212,7 +209,7 @@
 
     if (!result.ok) {
       cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
-        "Document preparation failure in directory " + dir)
+        "Failed to build document in directory " + File.path(dir.absolute_file))
     }
 
     bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
@@ -253,7 +250,10 @@
     val more_args = getopts(args)
     if (more_args.nonEmpty) getopts.usage()
 
-    build_document(document_dir = document_dir, document_name = document_name,
-      document_format = document_format, tags = tags)
+    try {
+      build_document(document_dir = document_dir, document_name = document_name,
+        document_format = document_format, tags = tags)
+    }
+    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
   })
 }