equal
deleted
inserted
replaced
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_response [display,gray] |
31 \<open>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)\<close> \<open>("timeout", ~1)\<close>} |
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, |
44 |
44 |
45 \<open>FOO=/usr/local/bin/foo\<close> |
45 \<open>FOO=/usr/local/bin/foo\<close> |
46 |
46 |
47 In Isabelle, this application may now be executed by |
47 In Isabelle, this application may now be executed by |
48 |
48 |
49 @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>} |
49 @{ML_response [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>} |
50 \<close> |
50 \<close> |
51 |
51 |
52 |
52 |
53 end |
53 end |