equal
deleted
inserted
replaced
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) Isabelle_System.bash_output \"sleep 30\" |
31 "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\" |
32 handle TimeLimit.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, |
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 |