# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1222908175 14400
# Node ID 1c17e99f6f669759d0aee1e1944c0fb1f5f360ec
# Parent  2b07da8b310d27527ca1b5e17a7a877f73e15c78
added a paragraph about "uses" and started a paragraph about tracing

diff -r 2b07da8b310d -r 1c17e99f6f66 CookBook/FirstSteps.thy
--- 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 {* 
   
diff -r 2b07da8b310d -r 1c17e99f6f66 CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Wed Oct 01 20:09:45 2008 -0400
+++ b/CookBook/Recipes/NamedThms.thy	Wed Oct 01 20:42:55 2008 -0400
@@ -28,7 +28,7 @@
 text {*
   This declares a context data slot where the theorems are stored,
   an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
-  to declare new rules, and the internal ML interface to retrieve and 
+  to declare new rules) and the internal ML interface to retrieve and 
   modify the facts.
 
   Furthermore, the facts are made available under the dynamic fact name
diff -r 2b07da8b310d -r 1c17e99f6f66 cookbook.pdf
Binary file cookbook.pdf has changed