equal
deleted
inserted
replaced
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 *) |