--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,55 @@
+theory ExternalSolver
+imports "../Base"
+begin
+
+
+section {* Executing an External Application \label{rec:external}*}
+
+text {*
+  {\bf Problem:}
+  You want to use an external application.
+  \smallskip
+
+  {\bf Solution:} The function @{ML system_out} might be the right thing for
+  you.
+  \smallskip
+
+  This function executes an external command as if printed in a shell. It
+  returns the output of the program and its return value.
+
+  For example, consider running an ordinary shell commands:
+
+  @{ML_response [display,gray] 
+    "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+
+  Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
+  on Page~\pageref{rec:timeout}), i.e. external applications are killed
+  properly. For example, the following expression takes only approximately
+  one second:
+
+  @{ML_response [display,gray] 
+    "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
+     handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+*}
+
+text {*
+  The function @{ML system_out} can also be used for more reasonable
+  applications, e.g. coupling external solvers with Isabelle. In that case,
+  one has to make sure that Isabelle can find the particular executable.
+  One way to ensure this is by adding a Bash-like variable binding into
+  one of Isabelle's settings file (prefer the user settings file usually to
+  be found at @{text "$HOME/.isabelle/etc/settings"}).
+  
+  For example, assume you want to use the application @{text foo} which
+  is here supposed to be located at @{text "/usr/local/bin/"}.
+  The following line has to be added to one of Isabelle's settings file:
+
+  @{text "FOO=/usr/local/bin/foo"}
+
+  In Isabelle, this application may now be executed by
+
+  @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
+*}
+
+
+end
\ No newline at end of file