equal
deleted
inserted
replaced
46 err_lines = err_lines, |
46 err_lines = err_lines, |
47 timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
47 timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
48 end |
48 end |
49 | _ => raise Fail "Malformed Isabelle/Scala result"); |
49 | _ => raise Fail "Malformed Isabelle/Scala result"); |
50 |
50 |
|
51 val bash = bash_process #> Process_Result.print #> Process_Result.rc; |
|
52 |
51 fun bash_output s = |
53 fun bash_output s = |
52 let |
54 let |
53 val res = bash_process s; |
55 val res = bash_process s; |
54 val _ = warning (Process_Result.err res); |
56 val _ = warning (Process_Result.err res); |
55 in (Process_Result.out res, Process_Result.rc res) end; |
57 in (Process_Result.out res, Process_Result.rc res) end; |
56 |
|
57 fun bash s = |
|
58 let |
|
59 val (out, rc) = bash_output s; |
|
60 val _ = writeln out; |
|
61 in rc end; |
|
62 |
58 |
63 |
59 |
64 (* bash functions *) |
60 (* bash functions *) |
65 |
61 |
66 fun bash_functions () = |
62 fun bash_functions () = |