# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249457058 -7200
# Node ID 2ac9dc1a95b4f5fcdf7902ad02e0282fa9815c4e
# Parent  14173c0e8688e54dab8b0818b2fe48ccb59f172e
added a comment for printing out information and tuned some examples accordingly

diff -r 14173c0e8688 -r 2ac9dc1a95b4 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -267,6 +267,18 @@
 fun string_of_thms_no_vars ctxt thms =  
   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 
+  concatenates a list of strings and inserts newlines. 
+
+  @{ML_response [display, gray]
+  "cat_lines [\"foo\", \"bar\"]"
+  "\"foo\\nbar\""}
+*}
+
+
 section {* Combinators\label{sec:combinators} *}
 
 text {*
@@ -746,9 +758,9 @@
   val v2 = Var ((\"x1\", 3), @{typ bool})
   val v3 = Free (\"x\", @{typ bool})
 in
-  tracing (Syntax.string_of_term @{context} v1);
-  tracing (Syntax.string_of_term @{context} v2);
-  tracing (Syntax.string_of_term @{context} v3)
+  map (Syntax.string_of_term @{context}) [v1, v2, v3]
+  |> cat_lines
+  |> tracing
 end"
 "?x3
 ?x1.3
diff -r 14173c0e8688 -r 2ac9dc1a95b4 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -615,8 +615,7 @@
         @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
         @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
 in 
-  s |> separate "\n"
-    |> implode
+  s |> cat_lines
     |> tracing
 end*}
 text_raw{*
diff -r 14173c0e8688 -r 2ac9dc1a95b4 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -551,13 +551,13 @@
   val string_of_prems = string_of_thms_no_vars context prems   
   val string_of_schms = string_of_cterms context (map fst (snd schematics))    
  
-  val _ = (tracing ("params: " ^ string_of_params);
-           tracing ("schematics: " ^ string_of_schms);
-           tracing ("assumptions: " ^ string_of_asms);
-           tracing ("conclusion: " ^ string_of_concl);
-           tracing ("premises: " ^ string_of_prems))
+  val strs = ["params: " ^ string_of_params,
+              "schematics: " ^ string_of_schms,
+              "assumptions: " ^ string_of_asms,
+              "conclusion: " ^ string_of_concl,
+              "premises: " ^ string_of_prems]
 in
-  all_tac 
+  tracing (cat_lines strs); all_tac 
 end*}
 
 text_raw{*
diff -r 14173c0e8688 -r 2ac9dc1a95b4 progtutorial.pdf
Binary file progtutorial.pdf has changed