
diff -r 11851b20fb78 -r 5c211dd7e5ad ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sat May 09 13:55:25 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 09 18:50:01 2009 +0200
@@ -1697,11 +1697,10 @@
 
 text {*
   So far we printed out only plain strings without any formatting except for
-  occasional explicit line breaks using @{text [quotes] "\\n"}. This is
+  occasional explicit linebreaks using @{text [quotes] "\\n"}. This is
   sufficient for ``quick-and-dirty'' printouts. For something more
-  sophisticated, Isabelle includes an infrastructure for formatting text.
-  This infrastructure is quite useful for printing for example large formulae.  
-  It is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
+  sophisticated, Isabelle includes an infrastructure for properly formatting text.
+  This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
   its functions do not operate on @{ML_type string}s, but on instances of the
   type:
 
@@ -1714,7 +1713,7 @@
   "Pretty.str \"test\"" "String (\"test\", 4)"}
 
   where the result indicates that we transformed a string with length 4. Once
-  you have a pretty type, you can, for example, control where line breaks can
+  you have a pretty type, you can, for example, control where linebreaks may
   occur in case the text wraps over a line, or with how much indentation a
   text should be printed.  However, if you want to actually output the
   formatted text, you have to transform the pretty type back into a @{ML_type
@@ -1726,9 +1725,9 @@
 ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
 
 text {*
-  The point of the pretty-printing infrastructure is to give hints how to
-  layout text and let the system do the actual layout. Let us first explain
-  how you can insert places where a line break can occur. For this assume the
+  The point of the pretty-printing infrastructure is to give hints about how to
+  layout text and let Isabelle do the actual layout. Let us first explain
+  how you can insert places where a linebreak can occur. For this assume the
   following function that replicates a string n times:
 *}
 
@@ -1741,8 +1740,9 @@
 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 
 text {*
-  Since @{ML test_str} is a string spanning over more than one line, we 
-  obtain the ugly
+  We deliberately chosed a large string so that is spans over more than one line. 
+  If we print out the string using the usual ``quick-and-dirty'' method, then
+  we obtain the ugly output:
 
 @{ML_response_fake [display,gray]
 "writeln test_str"
@@ -1751,7 +1751,6 @@
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 
-  if we print the string by the usual ``quick-and-dirty'' method. 
   We obtain the same if we just use
 
 @{ML_response_fake [display,gray]
@@ -1762,11 +1761,11 @@
 oooooooooooooobaaaaaaaaaaaar"}
 
   However by using pretty types you have the ability to indicate a possible
-  line break for example at each space. You can achieve this with the function
+  linebreak for example at each space. You can achieve this with the function
   @{ML Pretty.breaks}, which expects a list of pretty types and inserts a
-  possible line break in between every two elements in this list. To print
-  this this list of pretty types as a single string, we concatenate them 
-  with the function @{ML Pretty.blk} as follows
+  possible linebreak in between every two elements in this list. To print
+  this list of pretty types as a single string, we concatenate them 
+  with the function @{ML Pretty.blk} as follows:
 
 
 @{ML_response_fake [display,gray]
@@ -1781,8 +1780,8 @@
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 
   Here the layout of @{ML test_str} is much more pleasing to the 
-  eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-indentation
-  of the printed string. If you increase the indentation, you obtain
+  eye. The @{ML "0"} in @{ML Pretty.blk} stands for no indentation
+  of the printed string. You can increase the indentation and obtain
   
 @{ML_response_fake [display,gray]
 "let
@@ -1811,7 +1810,7 @@
           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 
   If you want to print out a list of items separated by commas and 
-  have the line breaks handled properly, you can use the function 
+  have the linebreaks handled properly, you can use the function 
   @{ML Pretty.commas}. For example
 
 @{ML_response_fake [display,gray]
@@ -1825,8 +1824,8 @@
 100016, 100017, 100018, 100019, 100020"}
 
   where @{ML upto} generates a list of integers. You can print this
-  list out as an ``set'' enclosed inside @{text [quotes] "{"} and
-  @{text [quotes] "}"}, and separated by commas by using the function
+  list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
+  @{text [quotes] "}"}, and separated by commas using the function
   @{ML Pretty.enum}. For example
 *}
 
@@ -1846,10 +1845,11 @@
   from the second each new line as an indentation of 2.
   
   If you print something out which goes beyond the capabilities of the
-  standard function, you can do the formating yourself. Assume you want
-  to print out a list of items where like in English the last two items
-  are separated by @{text [quotes] "and"}. For this you can write the 
-  function
+  standard function, you can do realatively easily the formating
+  yourself. Assume you want to print out a list of items where like in ``English''
+  the last two items are separated by @{text [quotes] "and"}. For this you can
+  write the function
+
 *}
 
 ML %linenosgray{*fun and_list [] = []
@@ -1865,9 +1865,10 @@
 text {*
   where in Line 7 we print the beginning of the list and in Line
   8 the last item. We have to use @{ML "Pretty.brk 1"} in order
-  to insert a space (of length 1) before the @{text [quotes] "and"}
-  where we also want that a line break can occur. We do the
-  same ater the @{text [quotes] "and"}. This gives you
+  to insert a space (of length 1) before the 
+  @{text [quotes] "and"}. This space is also a pleace where a linebreak 
+  can occur. We do the same ater the @{text [quotes] "and"}. This gives you
+  for example
 
 @{ML_response_fake [display,gray]
 "let
@@ -1878,8 +1879,8 @@
 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
 and 22"}
 
-  Next we like to pretty print a term and its type. For this we use the
-  function @{text "tell_type"}:
+  Next we like to pretty-print a term and its type. For this we use the
+  function @{text "tell_type"}.
 *}
 
 ML %linenosgray{*fun tell_type ctxt t = 
@@ -1894,13 +1895,13 @@
 end*}
 
 text {*
-  In Line 3 we define a function that inserts possible linebreaks into 
-  an (English) text according to spaces. In Lines 4 and 5 we pretty print
+  In Line 3 we define a function that inserts according to spaces 
+  possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
   the term and its type using the functions @{ML Syntax.pretty_term} and
   @{ML Syntax.pretty_typ}. We also use the function @{ML Pretty.quote}
-  in order to enclose the term and type with quotes. In Line 9 we add the 
-  period right after the type without the possibility of a line break, 
-  because we do not want that a line break occurs there.
+  in order to enclose the term and type inside quotation marks. In Line 
+  9 we add a period right after the type without the possibility of a 
+  linebreak, because we do not want that a linebreak occurs there.
 
   Now you can write
 
@@ -1908,7 +1909,8 @@
   "tell_type @{context} @{term \"min (Suc 0)\"}"
   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
   
-  You can see the proper line breaking with the term
+  To see the proper linebreaking, you can try out the function on a bigger term 
+  and type.
 
   @{ML_response_fake [display,gray]
   "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
@@ -1931,9 +1933,9 @@
   What happens with big formulae?
 
   \begin{readmore}
-  The general infrastructure for pretty printing is implemented in 
+  The general infrastructure for pretty-printing is implemented in the file
   @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
-  contains pretty printing functions for terms, types, theorems and so on.
+  contains pretty-printing functions for terms, types, theorems and so on.
   \end{readmore}
 *}
 




