# HG changeset patch # User Christian Urban # Date 1241887801 -7200 # Node ID 5c211dd7e5add052a85d6edf4bdbf72e01821262 # Parent 11851b20fb786e930e23b308d5b59e347029b461 slight polishing 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 \ 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} *} diff -r 11851b20fb78 -r 5c211dd7e5ad progtutorial.pdf Binary file progtutorial.pdf has changed