equal
deleted
inserted
replaced
322 let |
322 let |
323 val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \ |
323 val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \ |
324 \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1"; |
324 \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1"; |
325 val doc_path = Path.append result_path (Path.ext format (Path.basic name)); |
325 val doc_path = Path.append result_path (Path.ext format (Path.basic name)); |
326 val _ = if verbose then writeln s else (); |
326 val _ = if verbose then writeln s else (); |
327 val (out, rc) = bash_output s; |
327 val (out, rc) = Isabelle_System.bash_output s; |
328 val _ = |
328 val _ = |
329 if not (File.exists doc_path) orelse rc <> 0 then |
329 if not (File.exists doc_path) orelse rc <> 0 then |
330 cat_error out ("Failed to build document " ^ quote (show_path doc_path)) |
330 cat_error out ("Failed to build document " ^ quote (show_path doc_path)) |
331 else if verbose then writeln out |
331 else if verbose then writeln out |
332 else (); |
332 else (); |