--- a/ProgTutorial/FirstSteps.thy	Tue May 05 03:21:49 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri May 08 17:11:57 2009 +0200
@@ -710,7 +710,8 @@
 
 text {*
   The reason is that you cannot pass the arguments @{term P} and @{term Q} 
-  into an antiquotation. For example the following does \emph{not} work.
+  into an antiquotation.\footnote{At least not at the moment.} For example 
+  the following does \emph{not} work.
 *}
 
 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
@@ -1696,13 +1697,132 @@
 
 text {*
   Isabelle has a pretty sphisticated pretty printing module. 
+
+  Loosely based on
+  D. C. Oppen, "Pretty Printing",
+  ACM Transactions on Programming Languages and Systems (1980), 465-483.
+  
+  Fixme
+
+  @{text [display, gray] "Pretty.T"}
+
+  Transforming a string into a pretty
+
 *}
 
+ML {* 
+fun rep n str = implode (replicate n str)
+*}
+
+ML {*
+val test_str = rep 10 "fooooooooooooooobaaaaaaaaaaaar "
+*}
+
+ML {* 
+fun pprint prt = writeln (Pretty.string_of prt)
+*}
+
+ML {* 
+fun pprint2 prt = priority (Pretty.string_of prt)
+*}
+
+
+ML {*
+pprint (Pretty.str test_str)  
+*}
+
+
+
+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 {* pprint (Pretty.blk (3, p_strs test_str)) *}
+
+ML {* Pretty.indent *}
+
+ML {* pprint (Pretty.indent 10 (Pretty.blk (3, p_strs test_str))) *}
+
+ML {* string_of_int *}
+
+ML {*
+pprint (Pretty.block (Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))
+*}
+
+ML {*
+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]
+      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 othere*}
+
+ML {*
+ pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))]))
+*}
+
+ML {* pprint2 (Pretty.str "foo"); pprint2 (Pretty.str "bar")
+*}
+
+
+text {* types, terms and text *}
+
+term "min (Suc 0)"
+
+ML {* fastype_of *}
+
+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 =)))))"}
+*}
+
+text {* does not break inside the term or type *}
+
+
+
+
+
+
+
 text {*
   @{ML Pretty.big_list},
-  @{ML Pretty.brk},
-  @{ML Pretty.block},
-  @{ML Pretty.chunks}
+
+  equations
+
+  colours
 *}
 
 section {* Misc (TBD) *}