added try;
authorwenzelm
Thu Oct 11 19:22:15 2001 +0200 (2001-10-11)
changeset 117210d60622b668f
parent 11720 5341e38309e8
child 11722 78cf55fd57c6
added try;
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/seq.ML	Thu Oct 11 19:22:00 2001 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Thu Oct 11 19:22:15 2001 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val empty: 'a seq
     1.5    val cons: 'a * 'a seq -> 'a seq
     1.6    val single: 'a -> 'a seq
     1.7 +  val try: ('a -> 'b) -> 'a -> 'b seq
     1.8    val hd: 'a seq -> 'a
     1.9    val tl: 'a seq -> 'a seq
    1.10    val chop: int * 'a seq -> 'a list * 'a seq
    1.11 @@ -73,6 +74,12 @@
    1.12  fun hd xq = #1 (the (pull xq))
    1.13  and tl xq = #2 (the (pull xq));
    1.14  
    1.15 +(*partial function as procedure*)
    1.16 +fun try f x =
    1.17 +  (case Library.try f x of
    1.18 +    Some y => single y
    1.19 +  | None => empty);
    1.20 +
    1.21  
    1.22  (*the list of the first n elements, paired with rest of sequence;
    1.23    if length of list is less than n, then sequence had less than n elements*)