# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1241795517 -7200
# Node ID 53112deda119d78767318b53d5c3ff70529b6c76
# Parent  dc95a56b19532c3954d773230d776d60cc562d8f
Jasmin and Christian added examples for the pretty-printing section

diff -r dc95a56b1953 -r 53112deda119 ProgTutorial/FirstSteps.thy
--- 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) *}
diff -r dc95a56b1953 -r 53112deda119 ProgTutorial/Package/Ind_Interface.thy
--- 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)
diff -r dc95a56b1953 -r 53112deda119 progtutorial.pdf
Binary file progtutorial.pdf has changed