equal
deleted
inserted
replaced
120 then there is a convenient, though again ``quick-and-dirty'', method for |
120 then there is a convenient, though again ``quick-and-dirty'', method for |
121 converting values into strings, namely the function @{ML PolyML.makestring}: |
121 converting values into strings, namely the function @{ML PolyML.makestring}: |
122 |
122 |
123 @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} |
123 @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} |
124 |
124 |
125 However, @{ML [index] makestring} only works if the type of what is converted is monomorphic |
125 However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic |
126 and not a function. |
126 and not a function. |
127 |
127 |
128 The function @{ML "writeln"} should only be used for testing purposes, because any |
128 The function @{ML "writeln"} should only be used for testing purposes, because any |
129 output this function generates will be overwritten as soon as an error is |
129 output this function generates will be overwritten as soon as an error is |
130 raised. For printing anything more serious and elaborate, the |
130 raised. For printing anything more serious and elaborate, the |