# HG changeset patch
# User wenzelm
# Date 1527281256 -7200
# Node ID b5d0318757f0a2376058549695140d84afe97b46
# Parent  867bd42b3f591a004f62b1436b27844f02af2d43
more examples;

diff -r 867bd42b3f59 -r b5d0318757f0 src/Doc/System/Environment.thy
--- 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>