# HG changeset patch
# User wenzelm
# Date 1219830590 -7200
# Node ID 359764333bf41747048ceb635875508ea82d535d
# Parent  d3c5ab88fdcd46ac223feec8a8292c05028eff48
Property lists.

diff -r d3c5ab88fdcd -r 359764333bf4 src/Pure/General/properties.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/properties.ML	Wed Aug 27 11:49:50 2008 +0200
@@ -0,0 +1,29 @@
+(*  Title:      Pure/General/properties.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Property lists.
+*)
+
+signature PROPERTIES =
+sig
+  type property = string * string
+  type T = property list
+  val defined: T -> string -> bool
+  val get: T -> string -> string option
+  val put: string * string -> T -> T
+  val remove: string -> T -> T
+end;
+
+structure Properties: PROPERTIES =
+struct
+
+type property = string * string;
+type T = property list;
+
+fun defined (props: T) name = AList.defined (op =) props name;
+fun get (props: T) name = AList.lookup (op =) props name;
+fun put prop (props: T) = AList.update (op =) prop props;
+fun remove name (props: T) = AList.delete (op =) name props;
+
+end;