--- a/ProgTutorial/General.thy	Tue Nov 17 20:36:18 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Nov 17 23:59:19 2009 +0100
@@ -187,23 +187,28 @@
 
   that is the pretty printed version of @{text "bool"}. However, in PolyML it is 
   easy to install your own pretty printer. With the function below we 
-  mimic the behaviour of the usual pretty printer for 
-  datatypes.\footnote{Thanks to David Matthews for providing this
-  code.}
+  mimic the behaviour of the usual pretty printer for datatypes (it 
+  uses pretty-printing functions which will be explained in more detail in 
+  Section~\ref{sec:pretty}).
 *}
 
-ML{*fun typ_raw_pretty_printer depth _ ty =
+ML{*fun raw_pp_typ ty =
 let
- fun cond str a =
-   if depth <= 0 
-   then PolyML.PrettyString "..."
-   else PolyML.PrettyBlock(1, false, [], 
-          [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a])
-in 
+  fun pp_pair (x1, x2) = Pretty.list "(" ")" [x1, x2]
+  fun pp_list xs = Pretty.list "[" "]" xs
+  fun pp_str s   = Pretty.str s
+  fun pp_qstr s  = Pretty.quote (pp_str s)
+  fun pp_int i   = pp_str (string_of_int i)
+  fun pp_sort S  = pp_list (map pp_qstr S)
+  fun pp_constr s xs = Pretty.block [pp_str s, Pretty.brk 1, xs]
+in
   case ty of
-    Type a  => cond "Type"  (PolyML.prettyRepresentation(a, depth - 1))
-  | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) 
-  | TVar a  => cond "TVar"  (PolyML.prettyRepresentation(a, depth - 1))
+    TVar ((a, i), S) => 
+      pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
+  | TFree (a, S) => 
+      pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
+  | Type (a, tys) => 
+      pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
 end*}
 
 text {*
@@ -211,23 +216,11 @@
   @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
 
-ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
-
-(*
-classes s
-
-ML {* @{typ "bool \<Rightarrow> ('a::s)"} *}
-
-ML {* 
-fun test ty =
-  case ty of
-    TVar ((v, n), s) => Pretty.block [Pretty.str "TVar "]
-  | TFree (x, s) => Pretty.block [Pretty.str "TFree "]
-  | Type (s, tys) => Pretty.block [Pretty.str "Type "]
-*}
-
-ML {* toplevel_pp ["typ"] "test" *}
-*)
+ML{*let
+  fun pp _ _ = ml_pretty o Pretty.to_ML o raw_pp_typ
+in
+  PolyML.addPrettyPrinter pp
+end*}
 
 text {*
   Now the type bool is printed out in full detail.
@@ -257,10 +250,11 @@
   with the code
 *}
 
-ML{*fun stnd_pretty_printer _ _ =   
-  ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy;
-
-PolyML.addPrettyPrinter stnd_pretty_printer*}
+ML{*let
+  fun pp _ _ = ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy
+in
+  PolyML.addPrettyPrinter pp
+end*}
 
 text {*
   After that the types for booleans, lists and so on are printed out again 
@@ -2089,6 +2083,9 @@
   valid local theory.
 
   @{ML "Context.>> o Context.map_theory"}
+
+  \footnote{\bf FIXME: list append in merge operations can cause 
+  exponential blowups.}
 *}
 
 section {* Setups (TBD) *}

--- a/ProgTutorial/Intro.thy	Tue Nov 17 20:36:18 2009 +0100
+++ b/ProgTutorial/Intro.thy	Tue Nov 17 23:59:19 2009 +0100
@@ -228,7 +228,7 @@
   are by him.
 
   \item {\bf Lukas Bulwahn} made me aware of the problems with recursive
-  parsers.
+  parsers and contributed exercise \ref{ex:contextfree}.
 
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.

--- a/ProgTutorial/Parsing.thy	Tue Nov 17 20:36:18 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Nov 17 23:59:19 2009 +0100
@@ -375,8 +375,8 @@
   \footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.} 
 
   Be aware of recursive parsers. Suppose you want to read strings
-  separated by commas and by parentheses into a tree. We assume 
-  the trees are represented by the datatype:
+  separated by commas and by parentheses into a tree datastructure. 
+  We assume the trees are represented by the datatype:
 *}
 
 ML{*datatype tree = 
@@ -409,7 +409,7 @@
   "*** Exception- TOPLEVEL_ERROR raised"}
 
   raises an exception indicating that the stack limit is reached. Such
-  looping parser are not useful at all, because of ML's strict evaluation of
+  looping parser are not useful, because of ML's strict evaluation of
   arguments. Therefore we need to delay the execution of the
   parser until an input is given. This can be done by adding the parsed
   string as an explicit argument.

Binary file progtutorial.pdf has changed