
diff -r 163ac0662211 -r a12bb28fe2bd ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Wed Oct 07 11:28:40 2009 +0200
+++ b/ProgTutorial/General.thy	Thu Oct 08 21:49:11 2009 +0200
@@ -1131,18 +1131,13 @@
     ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
 
 
-(* FIXME: some code below *)
-
-(*<*)
 (*
 setup {*
  Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
 *}
-*)
 lemma "bar = (1::nat)"
   oops
 
-(*
 setup {*   
   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  #> PureThy.add_defs false [((@{binding "foo_def"}, 
@@ -1157,7 +1152,7 @@
 
 thm foo_def
 *)
-(*>*)
+
 
 section {* Pretty-Printing\label{sec:pretty} *}
 
@@ -1165,10 +1160,9 @@
   So far we printed out only plain strings without any formatting except for
   occasional explicit line breaks using @{text [quotes] "\\n"}. This is
   sufficient for ``quick-and-dirty'' printouts. For something more
-  sophisticated, Isabelle includes an infrastructure for properly formatting text.
-  This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
-  its functions do not operate on @{ML_type string}s, but on instances of the
-  type:
+  sophisticated, Isabelle includes an infrastructure for properly formatting
+  text. Most of its functions do not operate on @{ML_type string}s, but on
+  instances of the pretty type:
 
   @{ML_type_ind [display, gray] "Pretty.T"}
 
@@ -1217,7 +1211,7 @@
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 
-  We obtain the same if we just use
+  We obtain the same if we just use the function @{ML pprint}.
 
 @{ML_response_fake [display,gray]
 "pprint (Pretty.str test_str)"
@@ -1226,13 +1220,12 @@
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 
-  However by using pretty types you have the ability to indicate a possible
-  line break for example at each space. You can achieve this with the function
-  @{ML_ind  breaks in Pretty}, which expects a list of pretty types and inserts a
-  possible line break in between every two elements in this list. To print
-  this list of pretty types as a single string, we concatenate them 
-  with the function @{ML_ind  blk in Pretty} as follows:
-
+  However by using pretty types you have the ability to indicate possible
+  linebreaks for example at each whitespace. You can achieve this with the
+  function @{ML_ind breaks in Pretty}, which expects a list of pretty types
+  and inserts a possible line break in between every two elements in this
+  list. To print this list of pretty types as a single string, we concatenate
+  them with the function @{ML_ind blk in Pretty} as follows:
 
 @{ML_response_fake [display,gray]
 "let
@@ -1308,7 +1301,7 @@
   100016, 100017, 100018, 100019, 100020}"}
 
   As can be seen, this function prints out the ``set'' so that starting 
-  from the second, each new line as an indentation of 2.
+  from the second, each new line has an indentation of 2.
   
   If you print out something that goes beyond the capabilities of the
   standard functions, you can do relatively easily the formatting
@@ -1338,12 +1331,16 @@
 
 @{ML_response_fake [display,gray]
 "let
-  val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
+  val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
+  val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
 in
-  pprint (Pretty.blk (0, and_list ptrs))
+  pprint (Pretty.blk (0, and_list ptrs1));
+  pprint (Pretty.blk (0, and_list ptrs2))
 end"
 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
-and 22"}
+and 22
+10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
+28"}
 
   Next we like to pretty-print a term and its type. For this we use the
   function @{text "tell_type"}.
@@ -1368,8 +1365,6 @@
   Pretty} in order to enclose the term and type inside quotation marks. In
   Line 9 we add a period right after the type without the possibility of a
   line break, because we do not want that a line break occurs there.
-
-
   Now you can write
 
   @{ML_response_fake [display,gray]
@@ -1384,19 +1379,72 @@
   "The term \"op = (op = (op = (op = (op = op =))))\" has type 
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 
+  The function @{ML_ind big_list in Pretty} helps with printing long lists.
+  It is used for example in the command \isacommand{print\_theorems}. An
+  example is as follows.
 
-  FIXME: TBD below
+  @{ML_response_fake [display,gray]
+  "let
+  val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
+in
+  pprint (Pretty.big_list \"header\" pstrs)
+end"
+  "header
+  4
+  5
+  6
+  7
+  8
+  9
+  10"}
+
+  Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
+  a list of items, but automatically inserts forced breaks between each item.
+  Compare
+
+  @{ML_response_fake [display,gray]
+  "let
+  val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+in
+  pprint (Pretty.blk (0, a_and_b));
+  pprint (Pretty.chunks a_and_b)
+end"
+"ab
+a
+b"}
+  
+  \footnote{\bf What happens with printing big formulae?}
+
+  
+
+  \begin{readmore}
+  The general infrastructure for pretty-printing is implemented in the file
+  @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
+  contains pretty-printing functions for terms, types, theorems and so on.
+  
+  @{ML_file "Pure/General/markup.ML"}
+  \end{readmore}
 *}
 
-ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}
-
+(*
 text {*
-chunks inserts forced breaks (unlike blk where you have to do this yourself)
+  printing into the goal buffer as part of the proof state
 *}
 
-ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], 
-       Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *}
+text {* writing into the goal buffer *}
+
+ML {* fun my_hook interactive state =
+         (interactive ? Proof.goal_message (fn () => Pretty.str  
+"foo")) state
+*}
 
+setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
+
+lemma "False"
+oops
+*)
+
+(*
 ML {*
 fun setmp_show_all_types f =
    setmp show_all_types
@@ -1409,7 +1457,7 @@
              [(setmp show_question_marks false o setmp_show_all_types)
                   (Syntax.pretty_term ctxt) t1,
               Pretty.str "=", Syntax.pretty_term ctxt t2]);
-pty |> Pretty.string_of |> priority
+pty |> Pretty.string_of  
 *}
 
 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
@@ -1417,44 +1465,7 @@
 
 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-
-ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-text {*
-  Still to be done:
-
-  What happens with big formulae?
-
-  \begin{readmore}
-  The general infrastructure for pretty-printing is implemented in the file
-  @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
-  contains pretty-printing functions for terms, types, theorems and so on.
-  
-  @{ML_file "Pure/General/markup.ML"}
-  \end{readmore}
-*}
-
-text {*
-  printing into the goal buffer as part of the proof state
-*}
-
-
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-text {* writing into the goal buffer *}
-
-ML {* fun my_hook interactive state =
-         (interactive ? Proof.goal_message (fn () => Pretty.str  
-"foo")) state
-*}
-
-setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
-
-lemma "False"
-oops
+*)
 
 
 section {* Misc (TBD) *}




