isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:11851b20fb78
+:5c211dd7e5ad
 section {* Pretty-Printing\label{sec:pretty} *}
 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.
+sophisticated, Isabelle includes an infrastructure for properly formatting text.
-This infrastructure is quite useful for printing for example large formulae.
+This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
-It 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:
 @{ML_type [display, gray] "Pretty.T"}
 @{ML_response_fake [display,gray]
 "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
 string}. This can be done with the function @{ML Pretty.string_of}. In what
 follows we will use the following wrapper function for printing a pretty
 *}
 ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
 text {*
-The point of the pretty-printing infrastructure is to give hints how to
+The point of the pretty-printing infrastructure is to give hints about how to
-layout text and let the system do the actual layout. Let us first explain
+layout text and let Isabelle do the actual layout. Let us first explain
-how you can insert places where a line break can occur. For this assume the
+how you can insert places where a linebreak can occur. For this assume the
 following function that replicates a string n times:
 *}
 ML{*fun rep n str = implode (replicate n str) *}
 *}
 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 text {*
-Since @{ML test_str} is a string spanning over more than one line, we
+We deliberately chosed a large string so that is spans over more than one line.
-obtain the ugly
+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"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 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]
 "pprint (Pretty.str test_str)"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 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
+possible linebreak in between every two elements in this list. To print
-this this list of pretty types as a single string, we concatenate them
+this list of pretty types as a single string, we concatenate them
-with the function @{ML Pretty.blk} as follows
+with the function @{ML Pretty.blk} as follows:
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 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
+eye. The @{ML "0"} in @{ML Pretty.blk} stands for no indentation
-of the printed string. If you increase the indentation, you obtain
+of the printed string. You can increase the indentation and obtain
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 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]
 "let
 val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 "99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
 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
+list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
-@{text [quotes] "}"}, and separated by commas by using the function
+@{text [quotes] "}"}, and separated by commas using the function
 @{ML Pretty.enum}. For example
 *}
 text {*
 As can be seen, this function prints out the ``set'' so that starting
 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
+standard function, you can do realatively easily the formating
-to print out a list of items where like in English the last two items
+yourself. Assume you want to print out a list of items where like in ``English''
-are separated by @{text [quotes] "and"}. For this you can write the
+the last two items are separated by @{text [quotes] "and"}. For this you can
-function
+write the function
 *}
 ML %linenosgray{*fun and_list [] = []
 | and_list [x] = [x]
 | and_list xs =
 end *}
 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"}
+to insert a space (of length 1) before the
-where we also want that a line break can occur. We do the
+@{text [quotes] "and"}. This space is also a pleace where a linebreak
-same ater the @{text [quotes] "and"}. This gives you
+can occur. We do the same ater the @{text [quotes] "and"}. This gives you
+for example
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
 in
 pprint (Pretty.blk (0, and_list ptrs))
 end"
 "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
+Next we like to pretty-print a term and its type. For this we use the
-function @{text "tell_type"}:
+function @{text "tell_type"}.
 *}
 ML %linenosgray{*fun tell_type ctxt t =
 let
 fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
 (pstr "The term " @ [ptrm] @ pstr " has type "
 @ [pty, Pretty.str "."])))
 end*}
 text {*
-In Line 3 we define a function that inserts possible linebreaks into
+In Line 3 we define a function that inserts according to spaces
-an (English) text according to spaces. In Lines 4 and 5 we pretty print
+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
+in order to enclose the term and type inside quotation marks. In Line
-period right after the type without the possibility of a line break,
+9 we add a period right after the type without the possibility of a
-because we do not want that a line break occurs there.
+linebreak, because we do not want that a linebreak occurs there.
 Now you can write
 @{ML_response_fake [display,gray]
 "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 =))))\"}"
 "The term \"op = (op = (op = (op = (op = op =))))\" has type
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 colours
 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}
 *}
 section {* Misc (TBD) *}

changeset 249	5c211dd7e5ad
parent 248	11851b20fb78
child 250	ab9e09076462