src/Pure/basis.ML
changeset 2862 3f38cbd57d47
parent 2470 273580d5c040
child 2884 4f2a4c27f9b5
     1.1 --- a/src/Pure/basis.ML	Wed Apr 02 11:30:48 1997 +0200
     1.2 +++ b/src/Pure/basis.ML	Wed Apr 02 11:32:48 1997 +0200
     1.3 @@ -18,6 +18,23 @@
     1.4      | toString false = "false"
     1.5    end;
     1.6  
     1.7 +structure General =
     1.8 +  struct
     1.9 +  exception Option
    1.10 +
    1.11 +  datatype 'a option = NONE | SOME of 'a
    1.12 +
    1.13 +  fun getOpt (SOME v, _) = v
    1.14 +    | getOpt (NONE,   a) = a
    1.15 +
    1.16 +  fun isSome (SOME _) = true 
    1.17 +    | isSome NONE     = false
    1.18 +
    1.19 +  fun valOf (SOME v) = v
    1.20 +    | valOf NONE     = raise Option
    1.21 +  end;
    1.22 +
    1.23 +
    1.24  structure Int =
    1.25    struct
    1.26    fun toString (i: int) = makestring i;
    1.27 @@ -53,6 +70,11 @@
    1.28  
    1.29    fun concat []      = []
    1.30      | concat (l::ls) = l @ concat ls;
    1.31 +
    1.32 +  fun mapPartial f []      = []
    1.33 +    | mapPartial f (x::xs) = 
    1.34 +         (case f x of General.NONE   => mapPartial f xs
    1.35 +                    | General.SOME y => y :: mapPartial f xs);
    1.36    end;
    1.37  
    1.38