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_matchresult [display,gray] |
22 @{ML_matchresult [display,gray] |
23 "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"} |
23 \<open>Isabelle_System.bash_output "echo Hello world!"\<close> \<open>("Hello world!\n", 0)\<close>} |
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_matchresult_fake [display,gray] |
30 @{ML_matchresult_fake [display,gray] |
31 "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\" |
31 \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30" |
32 handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
32 handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>} |
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, |
36 one has to make sure that Isabelle can find the particular executable. |
36 one has to make sure that Isabelle can find the particular executable. |
37 One way to ensure this is by adding a Bash-like variable binding into |
37 One way to ensure this is by adding a Bash-like variable binding into |