17 This function executes an external command as if printed in a shell. It |
17 This function executes an external command as if printed in a shell. It |
18 returns the output of the program and its return value. |
18 returns the output of the program and its return value. |
19 |
19 |
20 For example, consider running an ordinary shell commands: |
20 For example, consider running an ordinary shell commands: |
21 |
21 |
22 @{ML_response [display,gray] |
22 @{ML_matchresult [display,gray] |
23 "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"} |
23 "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"} |
24 |
24 |
25 Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout} |
25 Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout} |
26 on Page~\pageref{rec:timeout}), i.e. external applications are killed |
26 on Page~\pageref{rec:timeout}), i.e. external applications are killed |
27 properly. For example, the following expression takes only approximately |
27 properly. For example, the following expression takes only approximately |
28 one second: |
28 one second: |
29 |
29 |
30 @{ML_response_fake [display,gray] |
30 @{ML_matchresult_fake [display,gray] |
31 "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\" |
31 "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\" |
32 handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
32 handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
33 |
33 |
34 The function @{ML bash_output in Isabelle_System} can also be used for more reasonable |
34 The function @{ML bash_output in Isabelle_System} can also be used for more reasonable |
35 applications, e.g. coupling external solvers with Isabelle. In that case, |
35 applications, e.g. coupling external solvers with Isabelle. In that case, |