# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249480801 -7200
# Node ID fe732e890d87ac4679d7687acbcb6be10646aa84
# Parent  2ac9dc1a95b4f5fcdf7902ad02e0282fa9815c4e
tuned the section about printing several bits of inormation

diff -r 2ac9dc1a95b4 -r fe732e890d87 IsaMakefile
--- a/IsaMakefile	Wed Aug 05 09:24:18 2009 +0200
+++ b/IsaMakefile	Wed Aug 05 16:00:01 2009 +0200
@@ -23,6 +23,7 @@
           ProgTutorial/Package/*.ML
 	@rm -rf ProgTutorial/generated/* 
 	$(USEDIR) HOL ProgTutorial
+	hg parent --template '{date|shortdate}' > ProgTutorial/generated/tip
 	$(ISATOOL) version > ProgTutorial/generated/version 
 	$(ML_HOME)/poly -v > ProgTutorial/generated/pversion
 	$(ISATOOL) document -o pdf  ProgTutorial/generated
diff -r 2ac9dc1a95b4 -r fe732e890d87 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Aug 05 09:24:18 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 16:00:01 2009 +0200
@@ -147,7 +147,9 @@
   fun strip ("\^A" :: _ :: cs) = strip cs
     | strip (c :: cs) = c :: strip cs
     | strip [] = [];
-in implode o strip o explode end;
+in 
+  implode o strip o explode 
+end
 
 fun redirect_tracing stream =
  Output.tracing_fn := (fn s =>
@@ -268,14 +270,34 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
-  When printing out several `parcels' of information that belong 
-  together you should try to keep this information together. For 
-  this you can use the function @{ML [index] cat_lines}, which 
+  When printing out several parcels of information that semantiaclly 
+  belong  together, like a warning message consisting of a term and
+  a type, you should try to keep this information together 
+  in a single string. So do not print out information as
+
+@{ML_response_fake [display,gray]
+"tracing \"First half,\"; 
+tracing \"and second half.\""
+"First half,
+and second half."}
+
+  but as a single string with appropriate formatting. For example
+
+@{ML_response_fake [display,gray]
+"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"First half,
+and second half."}
+  
+  To ease this kind of string manipulations, there are a number
+  of library functions. For example,  the function @{ML [index] cat_lines}
   concatenates a list of strings and inserts newlines. 
 
   @{ML_response [display, gray]
   "cat_lines [\"foo\", \"bar\"]"
   "\"foo\\nbar\""}
+
+  Section \ref{sec:pretty} will also explain infrastructure that helps 
+  with more elaborate pretty printing. 
 *}
 
 
diff -r 2ac9dc1a95b4 -r fe732e890d87 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Wed Aug 05 09:24:18 2009 +0200
+++ b/ProgTutorial/Intro.thy	Wed Aug 05 16:00:01 2009 +0200
@@ -233,7 +233,8 @@
   with TBD.}
 
   \vfill
-  This document was compiled with:\\
+  
+  This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\
   \input{version}\\
   \input{pversion}
 *}
diff -r 2ac9dc1a95b4 -r fe732e890d87 progtutorial.pdf
Binary file progtutorial.pdf has changed