--- a/src/Doc/System/Environment.thy Fri May 25 21:02:40 2018 +0200
+++ b/src/Doc/System/Environment.thy Fri May 25 22:47:36 2018 +0200
@@ -365,7 +365,7 @@
\<close>
-subsubsection \<open>Example\<close>
+subsubsection \<open>Examples\<close>
text \<open>
The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
@@ -375,6 +375,12 @@
Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
Isabelle/ML and Scala libraries provide functions for that, but here we need
to do it manually.
+
+ \<^medskip>
+ This is how to invoke a function body with proper return code and printing
+ of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
\<close>