diff -r afa2d9c6b3b7 -r 11851b20fb78 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sat May 09 03:11:36 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sat May 09 13:55:25 2009 +0200 @@ -1693,38 +1693,43 @@ *) (*>*) -section {* Pretty-Printing *} +section {* Pretty-Printing\label{sec:pretty} *} text {* - Isabelle has a sophisticated infrastructure for pretty-printing text - involving for example long formulae. This infrastructure is loosely based - on a paper by Oppen~\cite{Oppen80}. Most of its functions do not operate - directly on @{ML_type string}s, but on instances of the type: + So far we printed out only plain strings without any formatting except for + occasional explicit line breaks 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 + its functions do not operate on @{ML_type string}s, but on instances of the + type: @{ML_type [display, gray] "Pretty.T"} - The function @{ML "Pretty.str"} transforms a string into such a pretty + The function @{ML "Pretty.str"} transforms a (plain) string into such a pretty type. For example @{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 occur and 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 type: + 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 + 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 + type: *} ML{*fun pprint prt = writeln (Pretty.string_of prt)*} text {* - The point of the pretty-printing infrastructure is to aid the layout - of text. Let us first explain how you can insert places where a - line break can occur. For this assume the following function that - replicates a string n times: + 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 + following function that replicates a string n times: *} ML{*fun rep n str = implode (replicate n str) *} @@ -1736,7 +1741,8 @@ ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} text {* - If we use for printing the usial ``quick-and-dirty'' method + Since @{ML test_str} is a string spanning over more than one line, we + obtain the ugly @{ML_response_fake [display,gray] "writeln test_str" @@ -1745,7 +1751,8 @@ aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo oooooooooooooobaaaaaaaaaaaar"} - we obtain an ugly layout. Similarly if we just use + 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)" @@ -1754,15 +1761,13 @@ 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 + @{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 -text {* - We obtain better results if we indicate a possible line break at every - spece. You can achieve this with the function @{ML Pretty.breaks}, which - expects a list of pretty types and inserts a possible place for a - line break in between every two elements in this list. To print this - this list of pretty types we concatenate them with the function @{ML - Pretty.blk} as follows @{ML_response_fake [display,gray] "let @@ -1775,9 +1780,9 @@ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} - Here the layout of @{ML test_str} is much more pleaseing to the - eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-intendation - of the printed string. If we increase the intentation we obtain + 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 @{ML_response_fake [display,gray] "let @@ -1805,56 +1810,131 @@ 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 + @{ML Pretty.commas}. For example +@{ML_response_fake [display,gray] +"let + val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020) +in + pprint (Pretty.blk (0, Pretty.commas ptrs)) +end" +"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 + @{text [quotes] "}"}, and separated by commas by using the function + @{ML Pretty.enum}. For example +*} -ML{*fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str)) *} +text {* + +@{ML_response_fake [display,gray] +"let + val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020) +in + pprint (Pretty.enum \",\" \"{\" \"}\" ptrs) +end" +"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, + 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, + 100016, 100017, 100018, 100019, 100020}"} -ML{*pprint (Pretty.blk (0, Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))*} + 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 + 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{*fun and_list [] = [] +ML %linenosgray{*fun and_list [] = [] | and_list [x] = [x] | and_list xs = let val (front, last) = split_last xs in - (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] + (Pretty.commas front) @ + [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] end *} -ML{* pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) *} - -ML{* Pretty.enum "l" "r" "sep" *} - -text {* chunks = one ptr above the other*} - -ML{* pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))])) *} - -ML {* pprint (Pretty.str "foo"); pprint (Pretty.str "bar") *} - +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 -text {* types, terms and text *} +@{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"} -ML {*fun tell_type ctxt t = - pprint (Pretty.blk (0, (p_strs "The term ") - @ [Pretty.quote (Syntax.pretty_term ctxt t)] - @ p_strs " has type " - @ [Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)), Pretty.str "."]))*} - -ML{*tell_type @{context} @{term "min (Suc 0)"} *} - - -ML {* -tell_type @{context} @{term "(op =) ((op =) ((op =) ((op =) ((op =) (op =)))))"} + Next we like to pretty print a term and its type. For this we use the + function @{text "tell_type"}: *} -text {* does not break inside the term or type *} +ML %linenosgray{*fun tell_type ctxt t = +let + fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s)) + val ptrm = Pretty.quote (Syntax.pretty_term ctxt t) + val pty = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)) +in + pprint (Pretty.blk (0, + (pstr "The term " @ [ptrm] @ pstr " has type " + @ [pty, Pretty.str "."]))) +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 + 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. + + Now you can write + + @{ML_response_fake [display,gray] + "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 + + @{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 \ 'a \ bool) \ bool) \ bool) \ bool) \ bool) \ bool\"."} + +*} + +text {* + Still to be done: + @{ML Pretty.big_list}, + @{ML Pretty.chunks} + equations colours + + What happens with big formulae? + + \begin{readmore} + The general infrastructure for pretty printing is implemented in + @{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. + \end{readmore} *} section {* Misc (TBD) *}