--- 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