--- 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},