src/Pure/General/seq.ML
changeset 5558 64a8495201d1
parent 5014 32e6cab5e7d4
child 5864 30b6a3251813
equal deleted inserted replaced
5557:d6ceb4275742 5558:64a8495201d1
    35   val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    35   val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    36   val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    36   val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    37   val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    37   val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    38   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    38   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    39   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    39   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
       
    40   val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
    40 end;
    41 end;
    41 
    42 
    42 structure Seq: SEQ =
    43 structure Seq: SEQ =
    43 struct
    44 struct
    44 
    45 
   198           (case pull q of
   199           (case pull q of
   199             None => repq qs
   200             None => repq qs
   200           | Some (x, q) => rep (q :: qs) x);
   201           | Some (x, q) => rep (q :: qs) x);
   201   in fn x => make (fn () => rep [] x) end;
   202   in fn x => make (fn () => rep [] x) end;
   202 
   203 
       
   204 fun REPEAT1 f = THEN (f, REPEAT f);
       
   205 
   203 
   206 
   204 end;
   207 end;