# HG changeset patch # User Christian Urban # Date 1241831496 -7200 # Node ID afa2d9c6b3b7b6bf7b587bd7e54fab2dcb26ba4c # Parent eb81ab6da2a33c817ef77aa1ddaa962c6b853385 added some text to the pretty-printing section diff -r eb81ab6da2a3 -r afa2d9c6b3b7 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Fri May 08 17:21:20 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sat May 09 03:11:36 2009 +0200 @@ -1693,116 +1693,154 @@ *) (*>*) -section {* Pretty-Printing (TBD) *} +section {* Pretty-Printing *} + +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: + + @{ML_type [display, gray] "Pretty.T"} + + The function @{ML "Pretty.str"} transforms a 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: +*} + +ML{*fun pprint prt = writeln (Pretty.string_of prt)*} text {* - Isabelle has a pretty sphisticated pretty printing module. + 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: +*} + +ML{*fun rep n str = implode (replicate n str) *} + +text {* + and suppose we want to print out the string: +*} + +ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} - Loosely based on - D. C. Oppen, "Pretty Printing", - ACM Transactions on Programming Languages and Systems (1980), 465-483. - - Fixme +text {* + If we use for printing the usial ``quick-and-dirty'' method - @{text [display, gray] "Pretty.T"} +@{ML_response_fake [display,gray] +"writeln test_str" +"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo +ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa +aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo +oooooooooooooobaaaaaaaaaaaar"} - Transforming a string into a pretty + we obtain an ugly layout. Similarly 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"} *} -ML {* -fun rep n str = implode (replicate n str) -*} +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 {* -val test_str = rep 10 "fooooooooooooooobaaaaaaaaaaaar " -*} +@{ML_response_fake [display,gray] +"let + val ptrs = map Pretty.str (space_explode \" \" test_str) +in + pprint (Pretty.blk (0, Pretty.breaks ptrs)) +end" +"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar +fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar +fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar +fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} -ML {* -fun pprint prt = writeln (Pretty.string_of prt) -*} + 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 + +@{ML_response_fake [display,gray] +"let + val ptrs = map Pretty.str (space_explode \" \" test_str) +in + pprint (Pretty.blk (3, Pretty.breaks ptrs)) +end" +"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} -ML {* -fun pprint2 prt = priority (Pretty.string_of prt) -*} - + where starting from the second line the indent is 3. If you want + that every line starts with the same indent, you can use the + function @{ML Pretty.indent} as follows: -ML {* -pprint (Pretty.str test_str) -*} +@{ML_response_fake [display,gray] +"let + val ptrs = map Pretty.str (space_explode \" \" test_str) +in + pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs))) +end" +" fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar + fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} +*} -text {* string of (English) and breaks at each space *} - -ML {* -Pretty.blk -*} - -text {* integer is indent for the second and later lines*} - -ML {* -fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str)) -*} - -ML {* pprint (Pretty.blk (0, p_strs test_str)) *} +ML{*fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str)) *} -ML {* pprint (Pretty.blk (3, p_strs test_str)) *} - -ML {* Pretty.indent *} - -ML {* pprint (Pretty.indent 10 (Pretty.blk (3, p_strs test_str))) *} +ML{*pprint (Pretty.blk (0, Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))*} -ML {* string_of_int *} - -ML {* -pprint (Pretty.block (Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20)))) -*} - -ML {* -fun and_list [] = [] +ML{*fun and_list [] = [] | and_list [x] = [x] | and_list xs = - let val (front,last) = split_last xs + let + val (front, last) = split_last xs in (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] - end -*} + end *} -ML {* -pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) -*} +ML{* pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) *} -ML {* Pretty.enum "l" "r" "sep" *} +ML{* Pretty.enum "l" "r" "sep" *} -text {* chunks = one ptr above the othere*} +text {* chunks = one ptr above the other*} -ML {* - pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))])) -*} +ML{* pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))])) *} -ML {* pprint2 (Pretty.str "foo"); pprint2 (Pretty.str "bar") -*} +ML {* pprint (Pretty.str "foo"); pprint (Pretty.str "bar") *} text {* types, terms and text *} -term "min (Suc 0)" - -ML {* fastype_of *} - -ML {* -fun tell_type ctxt t = +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 "."])) - -*} + @ [Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)), Pretty.str "."]))*} -ML {* -tell_type @{context} @{term "min (Suc 0)"} -*} +ML{*tell_type @{context} @{term "min (Suc 0)"} *} ML {* @@ -1811,12 +1849,6 @@ text {* does not break inside the term or type *} - - - - - - text {* @{ML Pretty.big_list}, diff -r eb81ab6da2a3 -r afa2d9c6b3b7 ProgTutorial/document/root.bib --- a/ProgTutorial/document/root.bib Fri May 08 17:21:20 2009 +0200 +++ b/ProgTutorial/document/root.bib Sat May 09 03:11:36 2009 +0200 @@ -135,4 +135,13 @@ series = {Lecture Notes in Computer Science}, volume = {78}, year = {1979} -} \ No newline at end of file +} + +@Article{Oppen80, + author = {D.~C.~Oppen}, + title = {Pretty Printing}, + journal = {ACM Transactions on Programming Languages and Systems}, + year = {1980}, + pages = {465--483} +} + diff -r eb81ab6da2a3 -r afa2d9c6b3b7 progtutorial.pdf Binary file progtutorial.pdf has changed