--- a/CookBook/FirstSteps.thy	Wed Oct 01 20:09:45 2008 -0400
+++ b/CookBook/FirstSteps.thy	Wed Oct 01 20:42:55 2008 -0400
@@ -39,7 +39,11 @@
   \ldots
   \end{tabular}
   \end{center}
+*}
 
+section {* Inluding ML-Code *}
+
+text {*
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML} command. For example
 *}
@@ -64,16 +68,31 @@
   then Isabelle's undo operation has no effect on the definition of 
   @{ML "foo"}. 
 
-  (FIXME: add comment about including whole ML-files) 
+  Once a portion of code is relatively stable, one usually wants to 
+  export it to a separate ML-file. Such files can be included in a 
+  theory using @{ML_text "uses"} in the header of the theory.
+
+  \begin{center}
+  \begin{tabular}{@ {}l}
+  \isacommand{theory} CookBook\\
+  \isacommand{imports} Main\\
+  \isacommand{uses} @{text "\"file_to_be_included.ML\""}\\
+  \isacommand{begin}\\
+  \ldots
+  \end{tabular}
+  \end{center}
+*}
+
+section {* Debugging and Printing *}
+
+text {*
 
   During developments you might find it necessary to quickly inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
   the function @{ML "warning"}. For example 
 *}
 
-ML {*
-  val _ = warning "any string"
-*}
+ML {* warning "any string" *}
 
 text {*
   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
@@ -81,17 +100,47 @@
   converting arbitrary values into strings, for example: 
 *}
 
-ML {*
-  val _ = warning (makestring 1)
-*}
+ML {* warning (makestring 1) *}
 
 text {*
   However this only works if the type of what is printed is monomorphic and not 
   a function.
 *}
 
-text {* (FIXME: add here or in the appendix a comment about tracing) *}
-text {* (FIXME: maybe a comment about redirecting the trace information) *}
+text {* 
+  The funtion warning should only be used for testing purposes, because
+  the problem with this function is that any output will be
+  overwritten if an error is raised. For anything more serious 
+  the function @{ML tracing}, which writes all output in a separate
+  buffer, should be used.
+
+*}
+
+ML {* tracing "foo" *}
+
+text {* (FIXME: complete the comment about redirecting the trace information) 
+
+  In Isabelle it is possible to redirect the message channels to a 
+  separate file, e.g. to prevent Proof General from choking on massive 
+  amounts of trace output.
+
+*}
+
+ML {*
+  val strip_specials =
+  let
+    fun strip ("\^A" :: _ :: cs) = strip cs
+      | strip (c :: cs) = c :: strip cs
+      | strip [] = [];
+  in implode o strip o explode end;
+
+  fun redirect_tracing stream =
+  Output.tracing_fn := (fn s =>
+    (TextIO.output (stream, (strip_specials s));
+     TextIO.output (stream, "\n");
+     TextIO.flushOut stream));
+*}
+
 
 section {* Antiquotations *}
 
@@ -308,7 +357,7 @@
 
 
 
-section {* Type checking *}
+section {* Type Checking *}
 
 text {*