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 [display,gray] |
30 @{ML_response_fake [display,gray] |
31 "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\" |
31 "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\" |
32 handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
32 handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} |
33 *} |
|
34 |
33 |
35 text {* |
|
36 The function @{ML system_out} can also be used for more reasonable |
34 The function @{ML system_out} can also be used for more reasonable |
37 applications, e.g. coupling external solvers with Isabelle. In that case, |
35 applications, e.g. coupling external solvers with Isabelle. In that case, |
38 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. |
39 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 |
40 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 |