equal
deleted
inserted
replaced
32 let |
32 let |
33 val begin_cmt = Scan.this_string "(*" |
33 val begin_cmt = Scan.this_string "(*" |
34 val end_cmt = Scan.this_string "*)" |
34 val end_cmt = Scan.this_string "*)" |
35 in |
35 in |
36 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
36 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
37 >> (enclose "(**" "**)" o implode) |
37 >> (enclose "(**" "**)" o implode) |
38 end |
38 end |
39 |
39 |
40 val scan_all = |
40 val scan_all = |
41 Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
41 Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
42 >> implode #> fst |
42 >> implode #> fst |
43 *} |
43 *} |
44 |
44 |
45 text {* |
45 text {* |
46 By using @{ML_text "#> fst"} in the last line, the function |
46 By using @{text "#> fst"} in the last line, the function |
47 @{ML scan_all} retruns a string instead of a pair. For example: |
47 @{ML scan_all} retruns a string, instead of the pair a parser would |
|
48 normally return. For example: |
48 |
49 |
49 @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} |
50 @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} |
50 |
51 |
51 @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")" |
52 @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")" |
52 "\"foo (**test**) bar (**test**)\""} |
53 "\"foo (**test**) bar (**test**)\""} |