--- 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 \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 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) *}