equal
deleted
inserted
replaced
39 text {* |
39 text {* |
40 By using @{text "#> fst"} in the last line, the function |
40 By using @{text "#> fst"} in the last line, the function |
41 @{ML scan_all} retruns a string, instead of the pair a parser would |
41 @{ML scan_all} retruns a string, instead of the pair a parser would |
42 normally return. For example: |
42 normally return. For example: |
43 |
43 |
44 @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} |
44 @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""} |
45 |
45 |
46 @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")" |
46 @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")" |
47 "\"foo (**test**) bar (**test**)\""} |
47 "\"foo (**test**) bar (**test**)\""} |
48 |
48 |
49 *} |
49 *} |
50 |
50 |
51 end |
51 end |