src/Pure/Thy/present.ML
changeset 67187 3457d7d43ee9
parent 67180 dcac4659d482
child 67192 26f548370e8d
equal deleted inserted replaced
67186:a58bbe66ac81 67187:3457d7d43ee9
   195         " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
   195         " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
   196     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
   196     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
   197     val _ = if verbose then writeln script else ();
   197     val _ = if verbose then writeln script else ();
   198     val {out, err, rc, ...} = Bash.process script;
   198     val {out, err, rc, ...} = Bash.process script;
   199     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
   199     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
   200     val _ =
   200     val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
   201       if not (File.exists doc_path) orelse rc <> 0 then
       
   202         cat_error (trim_line err) ("Failed to build document " ^ quote (show_path doc_path))
       
   203       else ();
       
   204     val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   201     val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   205   in doc_path end;
   202   in doc_path end;
   206 
   203 
   207 
   204 
   208 (* finish session -- output all generated text *)
   205 (* finish session -- output all generated text *)