71 |
71 |
72 During development you might find it necessary to inspect some data |
72 During development you might find it necessary to inspect some data |
73 in your code. This can be done in a ``quick-and-dirty'' fashion using |
73 in your code. This can be done in a ``quick-and-dirty'' fashion using |
74 the function @{ML "warning"}. For example |
74 the function @{ML "warning"}. For example |
75 |
75 |
76 @{ML_response [display,gray] "warning \"any string\"" "\"any string\""} |
76 @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""} |
77 |
77 |
78 will print out @{text [quotes] "any string"} inside the response buffer |
78 will print out @{text [quotes] "any string"} inside the response buffer |
79 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
79 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
80 then there is a convenient, though again ``quick-and-dirty'', method for |
80 then there is a convenient, though again ``quick-and-dirty'', method for |
81 converting values into strings, namely the function @{ML makestring}: |
81 converting values into strings, namely the function @{ML makestring}: |
82 |
82 |
83 @{ML_response [display,gray] "warning (makestring 1)" "\"1\""} |
83 @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} |
84 |
84 |
85 However @{ML makestring} only works if the type of what is converted is monomorphic |
85 However @{ML makestring} only works if the type of what is converted is monomorphic |
86 and not a function. |
86 and not a function. |
87 |
87 |
88 The function @{ML "warning"} should only be used for testing purposes, because any |
88 The function @{ML "warning"} should only be used for testing purposes, because any |
89 output this function generates will be overwritten as soon as an error is |
89 output this function generates will be overwritten as soon as an error is |
90 raised. For printing anything more serious and elaborate, the |
90 raised. For printing anything more serious and elaborate, the |
91 function @{ML tracing} is more appropriate. This function writes all output into |
91 function @{ML tracing} is more appropriate. This function writes all output into |
92 a separate tracing buffer. For example: |
92 a separate tracing buffer. For example: |
93 |
93 |
94 @{ML_response [display,gray] "tracing \"foo\"" "\"foo\""} |
94 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} |
95 |
95 |
96 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
96 It is also possible to redirect the ``channel'' where the string @{text "foo"} is |
97 printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive |
97 printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive |
98 amounts of trace output. This redirection can be achieved with the code: |
98 amounts of trace output. This redirection can be achieved with the code: |
99 *} |
99 *} |
706 |
706 |
707 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
707 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
708 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
708 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
709 | is_nil_or_all _ = false *} |
709 | is_nil_or_all _ = false *} |
710 |
710 |
|
711 (* |
711 text {* |
712 text {* |
712 Occasional you have to calculate what the ``base'' name of a given |
713 Occasional you have to calculate what the ``base'' name of a given |
713 constant is. For this you can use the function @{ML Sign.extern_const} or |
714 constant is. For this you can use the function @{ML Sign.extern_const} or |
714 @{ML Sign.base_name}. For example: |
715 @{ML Sign.base_name}. For example: |
715 |
716 |