# HG changeset patch # User Christian Urban # Date 1239801068 0 # Node ID b63c72776f03597b71c8692e257affb3e674121d # Parent 29787dcf7b2eedfae6bf2f6226429c6a19533e8c replaced "warning" with "writeln" diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Base.thy --- 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 diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/FirstSteps.thy --- 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})" "\?P; ?Q\ \ ?P \ ?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})" "\P; Q\ \ P \ 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 \ int \ unit \ 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) *} diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Package/Ind_Code.thy --- 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} diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Recipes/Timing.thy --- 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 {* diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Solutions.thy --- 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 \"} with a term diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Tactical.thy --- 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*} diff -r 29787dcf7b2e -r b63c72776f03 progtutorial.pdf Binary file progtutorial.pdf has changed