8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 You want to use an external application. |
10 You want to use an external application. |
11 \smallskip |
11 \smallskip |
12 |
12 |
13 {\bf Solution:} The function @{ML system_out} might be the right thing for |
13 {\bf Solution:} The function @{ML bash_output} might be the right thing for |
14 you. |
14 you. |
15 \smallskip |
15 \smallskip |
16 |
16 |
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_response [display,gray] |
23 "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"} |
23 "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_response_fake [display,gray] |
31 "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\" |
31 "TimeLimit.timeLimit (Time.fromSeconds 1) bash_output \"sleep 30\" |
32 handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
32 handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
33 |
33 |
34 The function @{ML system_out} can also be used for more reasonable |
34 The function @{ML bash_output} 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 |
38 one of Isabelle's settings file (prefer the user settings file usually to |
38 one of Isabelle's settings file (prefer the user settings file usually to |
39 be found at @{text "$HOME/.isabelle/etc/settings"}). |
39 be found at @{text "$HOME/.isabelle/etc/settings"}). |