1696 section {* Pretty-Printing *}

  1696 section {* Pretty-Printing\label{sec:pretty} *}

  1697 

  1697 

  1698 text {*

  1698 text {*

  1699   Isabelle has a sophisticated infrastructure for pretty-printing text

  1699   So far we printed out only plain strings without any formatting except for

  1700   involving for example long formulae.  This infrastructure is loosely based

  1700   occasional explicit line breaks using @{text [quotes] "\\n"}. This is

  1701   on a paper by Oppen~\cite{Oppen80}. Most of its functions do not operate

  1701   sufficient for ``quick-and-dirty'' printouts. For something more

  1702   directly on @{ML_type string}s, but on instances of the type:

  1702   sophisticated, Isabelle includes an infrastructure for formatting text.

  1703   This infrastructure is quite useful for printing for example large formulae.  

  1704   It is loosely based on a paper by Oppen~\cite{Oppen80}. Most of

  1705   its functions do not operate on @{ML_type string}s, but on instances of the

  1706   type:

  1706   The function @{ML "Pretty.str"} transforms a string into such a pretty 

  1710   The function @{ML "Pretty.str"} transforms a (plain) string into such a pretty 

  1712   where the result indicates that we transformed a string with length 4. 

  1716   where the result indicates that we transformed a string with length 4. Once

  1713   Once you have a pretty type, you can, for example, control where line breaks 

  1717   you have a pretty type, you can, for example, control where line breaks can

  1714   can occur and with how much indentation a text should be printed.

  1718   occur in case the text wraps over a line, or with how much indentation a

  1715   However, if you want to actually output the formatted text, you have to 

  1719   text should be printed.  However, if you want to actually output the

  1716   transform the pretty type back into a @{ML_type string}. This can be done 

  1720   formatted text, you have to transform the pretty type back into a @{ML_type

  1717   with the  function @{ML Pretty.string_of}. In what follows we will use 

  1721   string}. This can be done with the function @{ML Pretty.string_of}. In what

  1718   the following wrapper function for printing a pretty type:

  1722   follows we will use the following wrapper function for printing a pretty

  1723   type:

  1724   The point of the pretty-printing infrastructure is to aid the layout 

  1729   The point of the pretty-printing infrastructure is to give hints how to

  1725   of text. Let us first explain how you can insert places where a

  1730   layout text and let the system do the actual layout. Let us first explain

  1726   line break can occur. For this assume the following function that 

  1731   how you can insert places where a line break can occur. For this assume the

  1727   replicates a string n times:

  1732   following function that replicates a string n times:

  1739   If we use for printing the usial ``quick-and-dirty'' method

  1744   Since @{ML test_str} is a string spanning over more than one line, we 

  1745   obtain the ugly

  1748   we obtain an ugly layout. Similarly if we just use

  1754   if we print the string by the usual ``quick-and-dirty'' method. 

  1755   We obtain the same if we just use

  1757 *}

  1764   However by using pretty types you have the ability to indicate a possible

  1758 

  1765   line break for example at each space. You can achieve this with the function

  1759 text {* 

  1766   @{ML Pretty.breaks}, which expects a list of pretty types and inserts a

  1760   We obtain better results if we indicate a possible line break at every

  1767   possible line break in between every two elements in this list. To print

  1761   spece. You can achieve this with the function @{ML Pretty.breaks}, which

  1768   this this list of pretty types as a single string, we concatenate them 

  1762   expects a list of pretty types and inserts a possible place for a 

  1769   with the function @{ML Pretty.blk} as follows

  1763   line break in between every two elements in this list. To print this

  1770 

  1764   this list of pretty types we concatenate them with the function @{ML

  1765   Pretty.blk} as follows

  1778   Here the layout of @{ML test_str} is much more pleaseing to the 

  1783   Here the layout of @{ML test_str} is much more pleasing to the 

  1779   eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-intendation

  1784   eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-indentation

  1780   of the printed string. If we increase the intentation we obtain

  1785   of the printed string. If you increase the indentation, you obtain

  1808 *} 

  1813   If you want to print out a list of items separated by commas and 

  1809 

  1814   have the line breaks handled properly, you can use the function 

  1810 

  1815   @{ML Pretty.commas}. For example

  1811 ML{*fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str)) *}

  1816 

  1812 

  1817 @{ML_response_fake [display,gray]

  1813 ML{*pprint (Pretty.blk (0, Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))*}

  1818 "let

  1814 

  1819   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)

  1815 ML{*fun and_list [] = []

  1820 in

  1821   pprint (Pretty.blk (0, Pretty.commas ptrs))

  1822 end"

  1823 "99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 

  1824 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 

  1825 100016, 100017, 100018, 100019, 100020"}

  1826 

  1827   where @{ML upto} generates a list of integers. You can print this

  1828   list out as an ``set'' enclosed inside @{text [quotes] "{"} and

  1829   @{text [quotes] "}"}, and separated by commas by using the function

  1830   @{ML Pretty.enum}. For example

  1831 *}

  1832 

  1833 text {*

  1834   

  1835 @{ML_response_fake [display,gray]

  1836 "let

  1837   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)

  1838 in

  1839   pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)

  1840 end"

  1841 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 

  1842   100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 

  1843   100016, 100017, 100018, 100019, 100020}"}

  1844 

  1845   As can be seen, this function prints out the ``set'' so that starting 

  1846   from the second each new line as an indentation of 2.

  1847   

  1848   If you print something out which goes beyond the capabilities of the

  1849   standard function, you can do the formating yourself. Assume you want

  1850   to print out a list of items where like in English the last two items

  1851   are separated by @{text [quotes] "and"}. For this you can write the 

  1852   function

  1853 *}

  1854 

  1855 ML %linenosgray{*fun and_list [] = []

  1821         (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]

  1861         (Pretty.commas front) @ 

  1862         [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]

  1824 ML{* pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) *}

  1865 text {*

  1825 

  1866   where in Line 7 we print the beginning of the list and in Line

  1826 ML{* Pretty.enum "l" "r" "sep" *}

  1867   8 the last item. We have to use @{ML "Pretty.brk 1"} in order

  1827 

  1868   to insert a space (of length 1) before the @{text [quotes] "and"}

  1828 text {* chunks = one ptr above the other*}

  1869   where we also want that a line break can occur. We do the

  1829 

  1870   same ater the @{text [quotes] "and"}. This gives you

  1830 ML{* pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))])) *}

  1871 

  1831 

  1872 @{ML_response_fake [display,gray]

  1832 ML {* pprint (Pretty.str "foo"); pprint (Pretty.str "bar") *}

  1873 "let

  1833 

  1874   val ptrs = map (Pretty.str o string_of_int) (1 upto 22)

  1834 

  1875 in

  1835 text {* types, terms and text *}

  1876   pprint (Pretty.blk (0, and_list ptrs))

  1836 

  1877 end"

  1837 ML {*fun tell_type ctxt t = 

  1878 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 

  1838   pprint (Pretty.blk (0, (p_strs "The term ") 

  1879 and 22"}

  1839                           @ [Pretty.quote (Syntax.pretty_term ctxt t)]

  1880 

  1840                           @ p_strs " has type " 

  1881   Next we like to pretty print a term and its type. For this we use the

  1841                           @ [Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)), Pretty.str "."]))*}

  1882   function @{text "tell_type"}:

  1842 

  1883 *}

  1843 ML{*tell_type @{context} @{term "min (Suc 0)"} *}

  1884 

  1844 

  1885 ML %linenosgray{*fun tell_type ctxt t = 

  1845 

  1886 let

  1846 ML {*

  1887   fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))

  1847 tell_type @{context} @{term "(op =) ((op =) ((op =) ((op =) ((op =) (op =)))))"}

  1888   val ptrm = Pretty.quote (Syntax.pretty_term ctxt t)

  1848 *}

  1889   val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t))

  1849 

  1890 in

  1850 text {* does not break inside the term or type *}

  1891   pprint (Pretty.blk (0, 

  1851 

  1892     (pstr "The term " @ [ptrm] @ pstr " has type " 

  1852 text {*

  1893       @ [pty, Pretty.str "."])))

  1894 end*}

  1895 

  1896 text {*

  1897   In Line 3 we define a function that inserts possible linebreaks into 

  1898   an (English) text according to spaces. In Lines 4 and 5 we pretty print

  1899   the term and its type using the functions @{ML Syntax.pretty_term} and

  1900   @{ML Syntax.pretty_typ}. We also use the function @{ML Pretty.quote}

  1901   in order to enclose the term and type with quotes. In Line 9 we add the 

  1902   period right after the type without the possibility of a line break, 

  1903   because we do not want that a line break occurs there.

  1904 

  1905   Now you can write

  1906 

  1907   @{ML_response_fake [display,gray]

  1908   "tell_type @{context} @{term \"min (Suc 0)\"}"

  1909   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}

  1910   

  1911   You can see the proper line breaking with the term

  1912 

  1913   @{ML_response_fake [display,gray]

  1914   "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"

  1915   "The term \"op = (op = (op = (op = (op = op =))))\" has type 

  1916 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}

  1917 

  1918 *}

  1919 

  1920 text {*

  1921   Still to be done:

  1922