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 |
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 \<open>$HOME/.isabelle/etc/settings\<close>). |
40 |
40 |
41 For example, assume you want to use the application @{text foo} which |
41 For example, assume you want to use the application \<open>foo\<close> which |
42 is here supposed to be located at @{text "/usr/local/bin/"}. |
42 is here supposed to be located at \<open>/usr/local/bin/\<close>. |
43 The following line has to be added to one of Isabelle's settings file: |
43 The following line has to be added to one of Isabelle's settings file: |
44 |
44 |
45 @{text "FOO=/usr/local/bin/foo"} |
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_response_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"} |
49 @{ML_response_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"} |
50 *} |
50 \<close> |
51 |
51 |
52 |
52 |
53 end |
53 end |