--- 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) *}

--- a/ProgTutorial/Package/Ind_Interface.thy	Tue May 05 03:21:49 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri May 08 17:11:57 2009 +0200
@@ -151,15 +151,11 @@
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we
   need for calling the package and setting up the keyword. The latter is
-  done in Lines 5 to 7 in the code below.
+  done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state 
+  here @{text "simple_inductive"}?}
 *}
-
-(*<*)
-ML %linenos 
-{* fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
-   fun add_inductive pred_specs rule_specs lthy = lthy *}
-(*>*)
-
+(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
+   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)
 ML_val %linenosgray{*val specification =
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)

Binary file progtutorial.pdf has changed