
diff -r eb81ab6da2a3 -r afa2d9c6b3b7 ProgTutorial/FirstSteps.thy
--- 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},
 




