--- a/ProgTutorial/Base.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Base.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -36,10 +36,5 @@
     (OuterParse.ML_source >> IsarCmd.ml_diag true);
 
 *}
-(*
-ML {*
-  fun warning str = str
-  fun tracing str = str
-*}
-*)
-end
+
+end
\ No newline at end of file

--- a/ProgTutorial/FirstSteps.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -95,21 +95,21 @@
 
   During development you might find it necessary to inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML "warning"}. For example 
+  the function @{ML "writeln"}. For example 
 
-  @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
+  @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, namely the function @{ML makestring}:
 
-  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] "writeln (makestring 1)" "\"1\""} 
 
   However, @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
 
-  The function @{ML "warning"} should only be used for testing purposes, because any
+  The function @{ML "writeln"} should only be used for testing purposes, because any
   output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
   function @{ML tracing} is more appropriate. This function writes all output into
@@ -173,10 +173,10 @@
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
   This produces a string with some additional information encoded in it. The string
-  can be properly printed by using the function @{ML warning}.
+  can be properly printed by using the function @{ML writeln}.
 
   @{ML_response_fake [display,gray]
-  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
   "\"1\""}
 
   A @{ML_type cterm} can be transformed into a string by the following function.
@@ -207,7 +207,7 @@
   @{text "?Q"} and so on. 
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm @{context} @{thm conjI})"
+  "writeln (str_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
   In order to improve the readability of theorems we convert
@@ -229,7 +229,7 @@
   Theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm_no_vars @{context} @{thm conjI})"
+  "writeln (str_of_thm_no_vars @{context} @{thm conjI})"
   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -333,7 +333,7 @@
   @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 
  |> Syntax.string_of_term @{context}
- |> warning"
+ |> writeln"
   "P z za zb"}
 
   You can read off this behaviour from how @{ML apply_fresh_args} is
@@ -1629,7 +1629,7 @@
          case realOut (!r) of
             NONE => "NONE"
           | SOME x => Real.toString x
-      val () = warning (concat [s1, " ", s2, " ", s3, "\n"])
+      val () = writeln (concat [s1, " ", s2, " ", s3, "\n"])
    end*}
 
 ML_val{*structure t = Test(U) *} 

--- a/ProgTutorial/Package/Ind_Code.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -50,7 +50,7 @@
   val arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
-  warning (str_of_thm_no_vars lthy' def); lthy'
+  writeln (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -117,7 +117,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  warning (Syntax.string_of_term lthy def); lthy
+  writeln (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
@@ -133,7 +133,7 @@
 *}
 
 local_setup %gray{* fn lthy =>
- (warning (Syntax.string_of_term lthy
+ (writeln (Syntax.string_of_term lthy
     (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
   lthy) *}
 
@@ -182,7 +182,7 @@
   val (defs, lthy') = 
     defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
-  warning (str_of_thms_no_vars lthy' defs); lthy
+  writeln (str_of_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -391,7 +391,7 @@
   val intro = 
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
-  warning (str_of_thm lthy intro); lthy
+  writeln (str_of_thm lthy intro); lthy
 end *}
 
 text {*
@@ -450,7 +450,7 @@
 let 
   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
-  warning (str_of_thms lthy ind_thms); lthy
+  writeln (str_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -516,7 +516,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  warning (str_of_thm_no_vars @{context} new_thm)
+  writeln (str_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -529,7 +529,7 @@
   @{thm [source] imp_elims_test}:
 
   @{ML_response_fake [display, gray]
-"warning (str_of_thm_no_vars @{context} 
+"writeln (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 
@@ -611,7 +611,7 @@
 in 
   s |> separate "\n"
     |> implode
-    |> warning
+    |> writeln
 end*}
 text_raw{*
 \end{isabelle}

--- a/ProgTutorial/Recipes/Timing.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Recipes/Timing.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -33,7 +33,7 @@
   val res = tac st;
   val t_end = end_timing t_start;
 in
-  (warning (#message t_end); res)
+  (writeln (#message t_end); res)
 end*}
 
 text {*

--- a/ProgTutorial/Solutions.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Solutions.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -170,7 +170,7 @@
   This function generates for example:
 
   @{ML_response_fake [display,gray] 
-  "warning (Syntax.string_of_term @{context} (term_tree 2))" 
+  "writeln (Syntax.string_of_term @{context} (term_tree 2))" 
   "(1 + 2) + (3 + 4)"} 
 
   The next function constructs a goal of the form @{text "P \<dots>"} with a term 

--- a/ProgTutorial/Tactical.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -210,7 +210,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = warning (str_of_thm_no_vars ctxt thm)
+  val _ = writeln (str_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -537,11 +537,11 @@
   val str_of_prems = str_of_thms_no_vars context prems   
   val str_of_schms = str_of_cterms context (snd schematics)    
  
-  val _ = (warning ("params: " ^ str_of_params);
-           warning ("schematics: " ^ str_of_schms);
-           warning ("assumptions: " ^ str_of_asms);
-           warning ("conclusion: " ^ str_of_concl);
-           warning ("premises: " ^ str_of_prems))
+  val _ = (writeln ("params: " ^ str_of_params);
+           writeln ("schematics: " ^ str_of_schms);
+           writeln ("assumptions: " ^ str_of_asms);
+           writeln ("conclusion: " ^ str_of_concl);
+           writeln ("premises: " ^ str_of_prems))
 in
   no_tac 
 end*}
@@ -583,7 +583,7 @@
   expects that the subgoal is solved completely.  Since in the function @{ML
   sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
   fails. The question-mark allows us to recover from this failure in a
-  graceful manner so that the warning messages are not overwritten by an 
+  graceful manner so that the output messages are not overwritten by an 
   ``empty sequence'' error message.
 
   If we continue the proof script by applying the @{text impI}-rule
@@ -1172,7 +1172,7 @@
 in
   s |> separate "\n"
     |> implode
-    |> warning
+    |> writeln
 end*}
 text_raw {* 
 \end{isabelle}
@@ -1494,7 +1494,7 @@
 ML %linenosgray{*fun fail_sp_aux simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+  val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
 in
   NONE
 end*}
@@ -1565,7 +1565,7 @@
 ML{*fun fail_sp_aux' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+  val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
 in
   NONE
 end*}

Binary file progtutorial.pdf has changed