--- 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}
*}