708 Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
708 Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
709 end *} |
709 end *} |
710 |
710 |
711 text {* |
711 text {* |
712 The reason is that you cannot pass the arguments @{term P} and @{term Q} |
712 The reason is that you cannot pass the arguments @{term P} and @{term Q} |
713 into an antiquotation. For example the following does \emph{not} work. |
713 into an antiquotation.\footnote{At least not at the moment.} For example |
|
714 the following does \emph{not} work. |
714 *} |
715 *} |
715 |
716 |
716 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *} |
717 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *} |
717 |
718 |
718 text {* |
719 text {* |
1694 |
1695 |
1695 section {* Pretty-Printing (TBD) *} |
1696 section {* Pretty-Printing (TBD) *} |
1696 |
1697 |
1697 text {* |
1698 text {* |
1698 Isabelle has a pretty sphisticated pretty printing module. |
1699 Isabelle has a pretty sphisticated pretty printing module. |
1699 *} |
1700 |
|
1701 Loosely based on |
|
1702 D. C. Oppen, "Pretty Printing", |
|
1703 ACM Transactions on Programming Languages and Systems (1980), 465-483. |
|
1704 |
|
1705 Fixme |
|
1706 |
|
1707 @{text [display, gray] "Pretty.T"} |
|
1708 |
|
1709 Transforming a string into a pretty |
|
1710 |
|
1711 *} |
|
1712 |
|
1713 ML {* |
|
1714 fun rep n str = implode (replicate n str) |
|
1715 *} |
|
1716 |
|
1717 ML {* |
|
1718 val test_str = rep 10 "fooooooooooooooobaaaaaaaaaaaar " |
|
1719 *} |
|
1720 |
|
1721 ML {* |
|
1722 fun pprint prt = writeln (Pretty.string_of prt) |
|
1723 *} |
|
1724 |
|
1725 ML {* |
|
1726 fun pprint2 prt = priority (Pretty.string_of prt) |
|
1727 *} |
|
1728 |
|
1729 |
|
1730 ML {* |
|
1731 pprint (Pretty.str test_str) |
|
1732 *} |
|
1733 |
|
1734 |
|
1735 |
|
1736 text {* string of (English) and breaks at each space *} |
|
1737 |
|
1738 ML {* |
|
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 [] = [] |
|
1764 | and_list [x] = [x] |
|
1765 | and_list xs = |
|
1766 let val (front,last) = split_last xs |
|
1767 in |
|
1768 (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] |
|
1769 end |
|
1770 *} |
|
1771 |
|
1772 ML {* |
|
1773 pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) |
|
1774 *} |
|
1775 |
|
1776 ML {* Pretty.enum "l" "r" "sep" *} |
|
1777 |
|
1778 text {* chunks = one ptr above the othere*} |
|
1779 |
|
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 *} |
|
1786 |
|
1787 |
|
1788 text {* types, terms and text *} |
|
1789 |
|
1790 term "min (Suc 0)" |
|
1791 |
|
1792 ML {* fastype_of *} |
|
1793 |
|
1794 ML {* |
|
1795 fun tell_type ctxt t = |
|
1796 pprint (Pretty.blk (0, (p_strs "The term ") |
|
1797 @ [Pretty.quote (Syntax.pretty_term ctxt t)] |
|
1798 @ p_strs " has type " |
|
1799 @ [Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)), Pretty.str "."])) |
|
1800 |
|
1801 *} |
|
1802 |
|
1803 ML {* |
|
1804 tell_type @{context} @{term "min (Suc 0)"} |
|
1805 *} |
|
1806 |
|
1807 |
|
1808 ML {* |
|
1809 tell_type @{context} @{term "(op =) ((op =) ((op =) ((op =) ((op =) (op =)))))"} |
|
1810 *} |
|
1811 |
|
1812 text {* does not break inside the term or type *} |
|
1813 |
|
1814 |
|
1815 |
|
1816 |
|
1817 |
|
1818 |
1700 |
1819 |
1701 text {* |
1820 text {* |
1702 @{ML Pretty.big_list}, |
1821 @{ML Pretty.big_list}, |
1703 @{ML Pretty.brk}, |
1822 |
1704 @{ML Pretty.block}, |
1823 equations |
1705 @{ML Pretty.chunks} |
1824 |
|
1825 colours |
1706 *} |
1826 *} |
1707 |
1827 |
1708 section {* Misc (TBD) *} |
1828 section {* Misc (TBD) *} |
1709 |
1829 |
1710 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |
1830 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |