equal
deleted
inserted
replaced
1941 *} |
1941 *} |
1942 |
1942 |
1943 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} |
1943 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} |
1944 |
1944 |
1945 text {* |
1945 text {* |
1946 We deliberately chose a large string so that is spans over more than one line. |
1946 We deliberately chose a large string so that it spans over more than one line. |
1947 If we print out the string using the usual ``quick-and-dirty'' method, then |
1947 If we print out the string using the usual ``quick-and-dirty'' method, then |
1948 we obtain the ugly output: |
1948 we obtain the ugly output: |
1949 |
1949 |
1950 @{ML_response_fake [display,gray] |
1950 @{ML_response_fake [display,gray] |
1951 "writeln test_str" |
1951 "writeln test_str" |