1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/properties.ML	Wed Aug 27 11:49:50 2008 +0200
     1.3 @@ -0,0 +1,29 @@
     1.4 +(*  Title:      Pure/General/properties.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Property lists.
     1.9 +*)
    1.10 +
    1.11 +signature PROPERTIES =
    1.12 +sig
    1.13 +  type property = string * string
    1.14 +  type T = property list
    1.15 +  val defined: T -> string -> bool
    1.16 +  val get: T -> string -> string option
    1.17 +  val put: string * string -> T -> T
    1.18 +  val remove: string -> T -> T
    1.19 +end;
    1.20 +
    1.21 +structure Properties: PROPERTIES =
    1.22 +struct
    1.23 +
    1.24 +type property = string * string;
    1.25 +type T = property list;
    1.26 +
    1.27 +fun defined (props: T) name = AList.defined (op =) props name;
    1.28 +fun get (props: T) name = AList.lookup (op =) props name;
    1.29 +fun put prop (props: T) = AList.update (op =) prop props;
    1.30 +fun remove name (props: T) = AList.delete (op =) name props;
    1.31 +
    1.32 +end;