diff -r 0b55402ae95e -r 126646f2aa88 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Mon Dec 15 10:48:27 2008 +0100 +++ b/CookBook/Solutions.thy Tue Dec 16 08:08:44 2008 +0000 @@ -23,4 +23,34 @@ HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} +text {* \solution{ex:scancmts} *} + +ML {* +val any = Scan.one (Symbol.not_eof); + +val scan_cmt = + let + val begin_cmt = Scan.this_string "(*" + val end_cmt = Scan.this_string "*)" + in + begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt + >> (enclose "(**" "**)" o implode) + end + +val scan_all = + Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) + >> implode #> fst +*} + +text {* + By using @{ML_text "#> fst"} in the last line, the function + @{ML scan_all} retruns a string instead of a pair. For example: + + @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} + + @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")" + "\"foo (**test**) bar (**test**)\""} + +*} + end \ No newline at end of file