CookBook/Solutions.thy
changeset 56 126646f2aa88
parent 47 4daf913fdbe1
child 58 f3794c231898
--- 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