more examples;
authorwenzelm
Fri May 25 22:47:36 2018 +0200 (20 months ago)
changeset 68275b5d0318757f0
parent 68274 867bd42b3f59
child 68276 cbee43ff4ceb
more examples;
src/Doc/System/Environment.thy
     1.1 --- a/src/Doc/System/Environment.thy	Fri May 25 21:02:40 2018 +0200
     1.2 +++ b/src/Doc/System/Environment.thy	Fri May 25 22:47:36 2018 +0200
     1.3 @@ -365,7 +365,7 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -subsubsection \<open>Example\<close>
     1.8 +subsubsection \<open>Examples\<close>
     1.9  
    1.10  text \<open>
    1.11    The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
    1.12 @@ -375,6 +375,12 @@
    1.13    Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
    1.14    Isabelle/ML and Scala libraries provide functions for that, but here we need
    1.15    to do it manually.
    1.16 +
    1.17 +  \<^medskip>
    1.18 +  This is how to invoke a function body with proper return code and printing
    1.19 +  of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
    1.20 +  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
    1.21 +  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
    1.22  \<close>
    1.23  
    1.24