93 |
93 |
94 text {* |
94 text {* |
95 |
95 |
96 During development you might find it necessary to inspect some data |
96 During development you might find it necessary to inspect some data |
97 in your code. This can be done in a ``quick-and-dirty'' fashion using |
97 in your code. This can be done in a ``quick-and-dirty'' fashion using |
98 the function @{ML "warning"}. For example |
98 the function @{ML "writeln"}. For example |
99 |
99 |
100 @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""} |
100 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} |
101 |
101 |
102 will print out @{text [quotes] "any string"} inside the response buffer |
102 will print out @{text [quotes] "any string"} inside the response buffer |
103 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
103 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
104 then there is a convenient, though again ``quick-and-dirty'', method for |
104 then there is a convenient, though again ``quick-and-dirty'', method for |
105 converting values into strings, namely the function @{ML makestring}: |
105 converting values into strings, namely the function @{ML makestring}: |
106 |
106 |
107 @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} |
107 @{ML_response_fake [display,gray] "writeln (makestring 1)" "\"1\""} |
108 |
108 |
109 However, @{ML makestring} only works if the type of what is converted is monomorphic |
109 However, @{ML makestring} only works if the type of what is converted is monomorphic |
110 and not a function. |
110 and not a function. |
111 |
111 |
112 The function @{ML "warning"} should only be used for testing purposes, because any |
112 The function @{ML "writeln"} should only be used for testing purposes, because any |
113 output this function generates will be overwritten as soon as an error is |
113 output this function generates will be overwritten as soon as an error is |
114 raised. For printing anything more serious and elaborate, the |
114 raised. For printing anything more serious and elaborate, the |
115 function @{ML tracing} is more appropriate. This function writes all output into |
115 function @{ML tracing} is more appropriate. This function writes all output into |
116 a separate tracing buffer. For example: |
116 a separate tracing buffer. For example: |
117 |
117 |
171 @{ML_response_fake [display,gray] |
171 @{ML_response_fake [display,gray] |
172 "Syntax.string_of_term @{context} @{term \"1::nat\"}" |
172 "Syntax.string_of_term @{context} @{term \"1::nat\"}" |
173 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} |
173 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} |
174 |
174 |
175 This produces a string with some additional information encoded in it. The string |
175 This produces a string with some additional information encoded in it. The string |
176 can be properly printed by using the function @{ML warning}. |
176 can be properly printed by using the function @{ML writeln}. |
177 |
177 |
178 @{ML_response_fake [display,gray] |
178 @{ML_response_fake [display,gray] |
179 "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})" |
179 "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})" |
180 "\"1\""} |
180 "\"1\""} |
181 |
181 |
182 A @{ML_type cterm} can be transformed into a string by the following function. |
182 A @{ML_type cterm} can be transformed into a string by the following function. |
183 *} |
183 *} |
184 |
184 |
205 text {* |
205 text {* |
206 Theorems also include schematic variables, such as @{text "?P"}, |
206 Theorems also include schematic variables, such as @{text "?P"}, |
207 @{text "?Q"} and so on. |
207 @{text "?Q"} and so on. |
208 |
208 |
209 @{ML_response_fake [display, gray] |
209 @{ML_response_fake [display, gray] |
210 "warning (str_of_thm @{context} @{thm conjI})" |
210 "writeln (str_of_thm @{context} @{thm conjI})" |
211 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
211 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
212 |
212 |
213 In order to improve the readability of theorems we convert |
213 In order to improve the readability of theorems we convert |
214 these schematic variables into free variables using the |
214 these schematic variables into free variables using the |
215 function @{ML Variable.import_thms}. |
215 function @{ML Variable.import_thms}. |
227 |
227 |
228 text {* |
228 text {* |
229 Theorem @{thm [source] conjI} is now printed as follows: |
229 Theorem @{thm [source] conjI} is now printed as follows: |
230 |
230 |
231 @{ML_response_fake [display, gray] |
231 @{ML_response_fake [display, gray] |
232 "warning (str_of_thm_no_vars @{context} @{thm conjI})" |
232 "writeln (str_of_thm_no_vars @{context} @{thm conjI})" |
233 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"} |
233 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"} |
234 |
234 |
235 Again the function @{ML commas} helps with printing more than one theorem. |
235 Again the function @{ML commas} helps with printing more than one theorem. |
236 *} |
236 *} |
237 |
237 |
331 variables to the function. For example: |
331 variables to the function. For example: |
332 |
332 |
333 @{ML_response_fake [display,gray] |
333 @{ML_response_fake [display,gray] |
334 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
334 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
335 |> Syntax.string_of_term @{context} |
335 |> Syntax.string_of_term @{context} |
336 |> warning" |
336 |> writeln" |
337 "P z za zb"} |
337 "P z za zb"} |
338 |
338 |
339 You can read off this behaviour from how @{ML apply_fresh_args} is |
339 You can read off this behaviour from how @{ML apply_fresh_args} is |
340 coded: in Line 2, the function @{ML fastype_of} calculates the type of the |
340 coded: in Line 2, the function @{ML fastype_of} calculates the type of the |
341 function; @{ML binder_types} in the next line produces the list of argument |
341 function; @{ML binder_types} in the next line produces the list of argument |
1627 | SOME i => Int.toString i |
1627 | SOME i => Int.toString i |
1628 val s3 = |
1628 val s3 = |
1629 case realOut (!r) of |
1629 case realOut (!r) of |
1630 NONE => "NONE" |
1630 NONE => "NONE" |
1631 | SOME x => Real.toString x |
1631 | SOME x => Real.toString x |
1632 val () = warning (concat [s1, " ", s2, " ", s3, "\n"]) |
1632 val () = writeln (concat [s1, " ", s2, " ", s3, "\n"]) |
1633 end*} |
1633 end*} |
1634 |
1634 |
1635 ML_val{*structure t = Test(U) *} |
1635 ML_val{*structure t = Test(U) *} |
1636 |
1636 |
1637 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*} |
1637 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*} |