diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML
+++ b/src/Pure/System/isabelle_system.ML
@@ -1,154 +1,150 @@
 (*  Title:      Pure/System/isabelle_system.ML
     Author:     Makarius
 
 Isabelle system support.
 *)
 
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: string -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
   val check_bash_function: Proof.context -> string * Position.T -> string
   val rm_tree: Path.T -> unit
   val make_directory: Path.T -> Path.T
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
   val copy_file: Path.T -> Path.T -> unit
   val copy_file_base: Path.T * Path.T -> Path.T -> unit
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val download: string -> string
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
 struct
 
 (* bash *)
 
 fun bash_process script =
   Scala.function_thread "bash_process"
     ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
   |> space_explode "\000"
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
           let
             val rc = Value.parse_int a;
             val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
             val (out_lines, err_lines) = chop (Value.parse_int d) lines;
           in
             Process_Result.make
              {rc = rc,
               out_lines = out_lines,
               err_lines = err_lines,
               timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
+val bash = bash_process #> Process_Result.print #> Process_Result.rc;
+
 fun bash_output s =
   let
     val res = bash_process s;
     val _ = warning (Process_Result.err res);
   in (Process_Result.out res, Process_Result.rc res) end;
 
-fun bash s =
-  let
-    val (out, rc) = bash_output s;
-    val _ = writeln out;
-  in rc end;
-
 
 (* bash functions *)
 
 fun bash_functions () =
   bash_process "declare -Fx"
   |> Process_Result.check
   |> Process_Result.out_lines
   |> map_filter (space_explode " " #> try List.last);
 
 fun check_bash_function ctxt arg =
   Completion.check_entity Markup.bash_functionN
     (bash_functions () |> map (rpair Position.none)) ctxt arg;
 
 
 (* directory operations *)
 
 fun system_command cmd =
   if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
 
 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
 
 fun make_directory path =
   let
     val _ =
       if File.is_dir path then ()
       else
        (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
         if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
   in path end;
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
 
 fun copy_dir src dst =
   if File.eq (src, dst) then ()
   else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
 
 fun copy_file src0 dst0 =
   let
     val src = Path.expand src0;
     val dst = Path.expand dst0;
     val target = if File.is_dir dst then dst + Path.base src else dst;
   in
     if File.eq (src, target) then ()
     else
       ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target))
   end;
 
 fun copy_file_base (base_dir, src0) target_dir =
   let
     val src = Path.expand src0;
     val src_dir = Path.dir src;
     val _ =
       if Path.starts_basic src then ()
       else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
   in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end;
 
 
 (* tmp files *)
 
 fun create_tmp_path name ext =
   let
     val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
     val _ = File.exists path andalso
       raise Fail ("Temporary file already exists: " ^ Path.print path);
   in path end;
 
 fun with_tmp_file name ext f =
   let val path = create_tmp_path name ext
   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
 
 (* tmp dirs *)
 
 fun with_tmp_dir name f =
   let val path = create_tmp_path name ""
   in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
 
 
 (* download file *)
 
 fun download url =
   with_tmp_file "download" "" (fn path =>
     let
       val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path;
       val res = bash_process s;
     in
       if Process_Result.ok res then File.read path
       else cat_error ("Failed to download " ^ quote url) (Process_Result.err res)
     end);
 
 end;
diff --git a/src/Pure/System/process_result.ML b/src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML
+++ b/src/Pure/System/process_result.ML
@@ -1,53 +1,59 @@
 (*  Title:      Pure/System/process_result.scala
     Author:     Makarius
 
 Result of system process.
 *)
 
 signature PROCESS_RESULT =
 sig
   type T
   val make:
    {rc: int,
     out_lines: string list,
     err_lines: string list,
     timing: Timing.timing} -> T
   val rc: T -> int
   val out_lines: T -> string list
   val err_lines: T -> string list
   val timing: T -> Timing.timing
   val out: T -> string
   val err: T -> string
   val ok: T -> bool
   val check: T -> T
+  val print: T -> T
 end;
 
 structure Process_Result: PROCESS_RESULT =
 struct
 
 abstype T =
   Process_Result of
    {rc: int,
     out_lines: string list,
     err_lines: string list,
     timing: Timing.timing}
 with
 
 val make = Process_Result;
 fun rep (Process_Result args) = args;
 
 val rc = #rc o rep;
 val out_lines = #out_lines o rep;
 val err_lines = #err_lines o rep;
 val timing = #timing o rep;
 
 end;
 
 val out = trim_line o cat_lines o out_lines;
 val err = trim_line o cat_lines o err_lines;
 
 fun ok result = rc result = 0;
 
 fun check result = if ok result then result else error (err result);
 
+fun print result =
+ (warning (err result);
+  writeln (out result);
+  make {rc = rc result, out_lines = [], err_lines = [], timing = timing result});
+
 end;