tuned messages;
authorwenzelm
Sun Dec 10 20:50:09 2017 +0100 (17 months ago)
changeset 67180dcac4659d482
parent 67179 35a4bf0f13b3
child 67181 0da2811afd87
tuned messages;
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
     1.1 --- a/src/Pure/Thy/present.ML	Sun Dec 10 20:31:14 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Dec 10 20:50:09 2017 +0100
     1.3 @@ -196,10 +196,10 @@
     1.4      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     1.5      val _ = if verbose then writeln script else ();
     1.6      val {out, err, rc, ...} = Bash.process script;
     1.7 -    val _ = if verbose then writeln (normalize_lines out) else ();
     1.8 +    val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
     1.9      val _ =
    1.10        if not (File.exists doc_path) orelse rc <> 0 then
    1.11 -        cat_error err ("Failed to build document " ^ quote (show_path doc_path))
    1.12 +        cat_error (trim_line err) ("Failed to build document " ^ quote (show_path doc_path))
    1.13        else ();
    1.14      val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
    1.15    in doc_path end;
     2.1 --- a/src/Pure/Thy/present.scala	Sun Dec 10 20:31:14 2017 +0100
     2.2 +++ b/src/Pure/Thy/present.scala	Sun Dec 10 20:50:09 2017 +0100
     2.3 @@ -182,10 +182,7 @@
     2.4        "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
     2.5  
     2.6      def bash(script: String): Process_Result =
     2.7 -    {
     2.8 -      Output.writeln(script)  // FIXME
     2.9        Isabelle_System.bash(script, cwd = dir.file)
    2.10 -    }
    2.11  
    2.12  
    2.13      /* prepare document */
    2.14 @@ -212,7 +209,7 @@
    2.15  
    2.16      if (!result.ok) {
    2.17        cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
    2.18 -        "Document preparation failure in directory " + dir)
    2.19 +        "Failed to build document in directory " + File.path(dir.absolute_file))
    2.20      }
    2.21  
    2.22      bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
    2.23 @@ -253,7 +250,10 @@
    2.24      val more_args = getopts(args)
    2.25      if (more_args.nonEmpty) getopts.usage()
    2.26  
    2.27 -    build_document(document_dir = document_dir, document_name = document_name,
    2.28 -      document_format = document_format, tags = tags)
    2.29 +    try {
    2.30 +      build_document(document_dir = document_dir, document_name = document_name,
    2.31 +        document_format = document_format, tags = tags)
    2.32 +    }
    2.33 +    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
    2.34    })
    2.35  }