src/HOL/Import/lazy_scan.ML

--- a/src/HOL/Import/lazy_scan.ML	Thu Feb 16 21:15:38 2006 +0100
+++ b/src/HOL/Import/lazy_scan.ML	Thu Feb 16 23:30:47 2006 +0100
@@ -29,6 +29,7 @@
     val option   : ('a,'b) scanner -> ('a,'b option) scanner
     val repeat   : ('a,'b) scanner -> ('a,'b list) scanner
     val repeat1  : ('a,'b) scanner -> ('a,'b list) scanner
+    val repeat_fixed : int -> ('a, 'b) scanner -> ('a, 'b list) scanner  
     val ahead    : ('a,'b) scanner -> ('a,'b) scanner
     val unless   : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
     val $$       : ''a -> (''a,''a) scanner
@@ -36,6 +37,8 @@
     val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
 
     val scan_id : (string, string) scanner
+    val scan_nat : (string, int) scanner
+
     val this : ''a list -> (''a, ''a list) scanner
     val this_string : string -> (string, string) scanner
 end
@@ -175,6 +178,15 @@
 	(x::xs,toks3)
     end
 
+fun repeat_fixed n sc =
+    let
+	fun R n xs toks =
+	    if (n <= 0) then (List.rev xs, toks)
+	    else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
+    in
+	R n []
+    end
+
 fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
 
 fun unless test sc toks =
@@ -208,6 +220,10 @@
 
 val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
 
+val nat_of_list = the o Int.fromString o implode 
+
+val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list 
+
 fun this [] = (fn toks => ([], toks))
   | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'