src/Pure/General/properties.ML
author wenzelm
Wed, 27 Aug 2008 11:49:50 +0200
changeset 28019 359764333bf4
child 28032 cb0021c989cd
permissions -rw-r--r--
Property lists.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/properties.ML
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     4
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     5
Property lists.
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     6
*)
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     7
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     8
signature PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     9
sig
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    10
  type property = string * string
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    11
  type T = property list
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    12
  val defined: T -> string -> bool
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    13
  val get: T -> string -> string option
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    14
  val put: string * string -> T -> T
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    15
  val remove: string -> T -> T
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    16
end;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    17
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    18
structure Properties: PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    19
struct
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    20
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    21
type property = string * string;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    22
type T = property list;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    23
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    24
fun defined (props: T) name = AList.defined (op =) props name;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    25
fun get (props: T) name = AList.lookup (op =) props name;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    26
fun put prop (props: T) = AList.update (op =) prop props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    27
fun remove name (props: T) = AList.delete (op =) name props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    28
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    29
end;