
diff -r afa2d9c6b3b7 -r 11851b20fb78 ProgTutorial/FirstSteps.thy
--- 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) *}




