tuned message;
authorwenzelm
Tue Dec 12 13:34:11 2017 +0100 (17 months ago)
changeset 671873457d7d43ee9
parent 67186 a58bbe66ac81
child 67188 bc7a6455e12a
tuned message;
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
     1.1 --- a/src/Pure/Thy/present.ML	Tue Dec 12 12:35:01 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Dec 12 13:34:11 2017 +0100
     1.3 @@ -197,10 +197,7 @@
     1.4      val _ = if verbose then writeln script else ();
     1.5      val {out, err, rc, ...} = Bash.process script;
     1.6      val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
     1.7 -    val _ =
     1.8 -      if not (File.exists doc_path) orelse rc <> 0 then
     1.9 -        cat_error (trim_line err) ("Failed to build document " ^ quote (show_path doc_path))
    1.10 -      else ();
    1.11 +    val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
    1.12      val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
    1.13    in doc_path end;
    1.14  
     2.1 --- a/src/Pure/Thy/present.scala	Tue Dec 12 12:35:01 2017 +0100
     2.2 +++ b/src/Pure/Thy/present.scala	Tue Dec 12 13:34:11 2017 +0100
     2.3 @@ -209,7 +209,7 @@
     2.4  
     2.5      if (!result.ok) {
     2.6        cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
     2.7 -        "Failed to build document in directory " + File.path(dir.absolute_file))
     2.8 +        "Failed to build document in " + File.path(dir.absolute_file))
     2.9      }
    2.10  
    2.11      bash("[ -f " + root_bash(document_format) + " ] && cp -f " +