140 @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"} |
140 @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"} |
141 |
141 |
142 will print out @{text [quotes] "any string"} inside the response buffer of |
142 will print out @{text [quotes] "any string"} inside the response buffer of |
143 Isabelle. This function expects a string as argument. If you develop under |
143 Isabelle. This function expects a string as argument. If you develop under |
144 PolyML, then there is a convenient, though again ``quick-and-dirty'', method |
144 PolyML, then there is a convenient, though again ``quick-and-dirty'', method |
145 for converting values into strings, namely the function |
145 for converting values into strings, namely the antiquotation |
146 @{ML_ind makestring in PolyML}: |
146 @{text "@{make_string}"}: |
147 |
147 |
148 @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} |
148 @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} |
149 |
149 |
150 However, @{ML makestring in PolyML} only works if the type of what |
150 However, @{text "@{makes_tring}"} only works if the type of what |
151 is converted is monomorphic and not a function. |
151 is converted is monomorphic and not a function. |
152 |
152 |
153 The function @{ML "writeln"} should only be used for testing purposes, |
153 The function @{ML "writeln"} should only be used for testing purposes, |
154 because any output this function generates will be overwritten as soon as an |
154 because any output this function generates will be overwritten as soon as an |
155 error is raised. For printing anything more serious and elaborate, the |
155 error is raised. For printing anything more serious and elaborate, the |
795 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
795 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
796 contains further information about combinators. |
796 contains further information about combinators. |
797 \end{readmore} |
797 \end{readmore} |
798 |
798 |
799 \footnote{\bf FIXME: find a good exercise for combinators} |
799 \footnote{\bf FIXME: find a good exercise for combinators} |
|
800 \begin{exercise} |
|
801 Find out what the combinator @{ML "K I"} does. |
|
802 \end{exercise} |
|
803 |
|
804 |
800 \footnote{\bf FIXME: say something about calling conventions} |
805 \footnote{\bf FIXME: say something about calling conventions} |
801 *} |
806 *} |
802 |
807 |
803 |
808 |
804 section {* ML-Antiquotations\label{sec:antiquote} *} |
809 section {* ML-Antiquotations\label{sec:antiquote} *} |