1696 section {* Pretty-Printing (TBD) *}

  1696 section {* Pretty-Printing *}

  1697 

  1697 

  1698 text {*

  1698 text {*

  1699   Isabelle has a pretty sphisticated pretty printing module. 

  1699   Isabelle has a sophisticated infrastructure for pretty-printing text

  1700 

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

  1701   Loosely based on

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

  1702   D. C. Oppen, "Pretty Printing",

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

  1703   ACM Transactions on Programming Languages and Systems (1980), 465-483.

  1703 

  1704   @{ML_type [display, gray] "Pretty.T"}

  1705 

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

  1707   type. For example

  1708 

  1709   @{ML_response_fake [display,gray]

  1710   "Pretty.str \"test\"" "String (\"test\", 4)"}

  1711 

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

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

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

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

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

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

  1718   the following wrapper function for printing a pretty type:

  1719 *}

  1720 

  1721 ML{*fun pprint prt = writeln (Pretty.string_of prt)*}

  1722 

  1723 text {*

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

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

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

  1727   replicates a string n times:

  1728 *}

  1729 

  1730 ML{*fun rep n str = implode (replicate n str) *}

  1731 

  1732 text {*

  1733   and suppose we want to print out the string:

  1734 *}

  1735 

  1736 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}

  1737 

  1738 text {*

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

  1740 

  1741 @{ML_response_fake [display,gray]

  1742 "writeln test_str"

  1743 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo

  1744 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa

  1745 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo

  1746 oooooooooooooobaaaaaaaaaaaar"}

  1747 

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

  1749 

  1750 @{ML_response_fake [display,gray]

  1751 "pprint (Pretty.str test_str)"

  1752 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo

  1753 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa

  1754 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo

  1755 oooooooooooooobaaaaaaaaaaaar"}

  1756 

  1757 *}

  1758 

  1759 text {* 

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

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

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

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

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

  1765   Pretty.blk} as follows

  1766 

  1767 @{ML_response_fake [display,gray]

  1768 "let

  1769   val ptrs = map Pretty.str (space_explode \" \" test_str)

  1770 in

  1771   pprint (Pretty.blk (0, Pretty.breaks ptrs))

  1772 end"

  1773 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1774 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1775 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar

  1776 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  1777 

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

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

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

  1705   Fixme

  1782 @{ML_response_fake [display,gray]

  1706 

  1783 "let

  1707   @{text [display, gray] "Pretty.T"}

  1784   val ptrs = map Pretty.str (space_explode \" \" test_str)

  1708 

  1785 in

  1709   Transforming a string into a pretty

  1786   pprint (Pretty.blk (3, Pretty.breaks ptrs))

  1710 

  1787 end"

  1711 *}

  1788 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1712 

  1789    fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1713 ML {* 

  1790    fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar

  1714 fun rep n str = implode (replicate n str)

  1791    fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  1715 *}

  1792 

  1716 

  1793   where starting from the second line the indent is 3. If you want

  1717 ML {*

  1794   that every line starts with the same indent, you can use the

  1718 val test_str = rep 10 "fooooooooooooooobaaaaaaaaaaaar "

  1795   function @{ML Pretty.indent} as follows:

  1719 *}

  1796 

  1720 

  1797 @{ML_response_fake [display,gray]

  1721 ML {* 

  1798 "let

  1722 fun pprint prt = writeln (Pretty.string_of prt)

  1799   val ptrs = map Pretty.str (space_explode \" \" test_str)

  1723 *}

  1800 in

  1724 

  1801   pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))

  1725 ML {* 

  1802 end"

  1726 fun pprint2 prt = priority (Pretty.string_of prt)

  1803 "          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1727 *}

  1804           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 

  1728 

  1805           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar

  1729 

  1806           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  1730 ML {*

  1807 

  1731 pprint (Pretty.str test_str)  

  1808 *} 

  1732 *}

  1809 

  1733 

  1810 

  1734 

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

  1735 

  1812 

  1736 text {* string of (English) and breaks at each space *}

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

  1737 

  1814 

  1738 ML {*

  1815 ML{*fun and_list [] = []

  1739 Pretty.blk  

  1740 *}

  1741 

  1742 text {* integer is indent for the second and later lines*}

  1743 

  1744 ML {*

  1745 fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str))

  1746 *}

  1747 

  1748 ML {* pprint (Pretty.blk (0, p_strs test_str)) *}

  1749 

  1750 ML {* pprint (Pretty.blk (3, p_strs test_str)) *}

  1751 

  1752 ML {* Pretty.indent *}

  1753 

  1754 ML {* pprint (Pretty.indent 10 (Pretty.blk (3, p_strs test_str))) *}

  1755 

  1756 ML {* string_of_int *}

  1757 

  1758 ML {*

  1759 pprint (Pretty.block (Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))

  1760 *}

  1761 

  1762 ML {*

  1763 fun and_list [] = []

  1766       let val (front,last) = split_last xs

  1818       let 

  1819         val (front, last) = split_last xs

  1769       end

  1822       end *}

  1770 *}

  1823 

  1771 

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

  1772 ML {*

  1825 

  1773 pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20))))

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

  1774 *}

  1827 

  1775 

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

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

  1829 

  1777 

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

  1778 text {* chunks = one ptr above the othere*}

  1831 

  1779 

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

  1780 ML {*

  1781  pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))]))

  1782 *}

  1783 

  1784 ML {* pprint2 (Pretty.str "foo"); pprint2 (Pretty.str "bar")

  1785 *}

  1790 term "min (Suc 0)"

  1837 ML {*fun tell_type ctxt t = 

  1791 

  1792 ML {* fastype_of *}

  1793 

  1794 ML {*

  1795 fun tell_type ctxt t = 

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

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

  1800 

  1842 

  1801 *}

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

  1802 

  1803 ML {*

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

  1805 *}