equal
deleted
inserted
replaced
100 @{ML_response_fake [display,gray] "writeln \"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 PolyML.makestring}: |
106 |
106 |
107 @{ML_response_fake [display,gray] "writeln (makestring 1)" "\"1\""} |
107 @{ML_response_fake [display,gray] "writeln (PolyML.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 "writeln"} should only be used for testing purposes, because any |
112 The function @{ML "writeln"} should only be used for testing purposes, because any |
369 |
369 |
370 *} |
370 *} |
371 |
371 |
372 ML %linenosgray{*fun inc_by_three x = |
372 ML %linenosgray{*fun inc_by_three x = |
373 x |> (fn x => x + 1) |
373 x |> (fn x => x + 1) |
374 |> tap (fn x => tracing (makestring x)) |
374 |> tap (fn x => tracing (PolyML.makestring x)) |
375 |> (fn x => x + 2)*} |
375 |> (fn x => x + 2)*} |
376 |
376 |
377 text {* |
377 text {* |
378 increments the argument first by @{text "1"} and then by @{text "2"}. In the |
378 increments the argument first by @{text "1"} and then by @{text "2"}. In the |
379 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' |
379 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' |