src/Pure/General/properties.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28032 cb0021c989cd
child 29606 fedb8be05f24
permissions -rw-r--r--
case default fallback for NBE
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
28032
cb0021c989cd added get_int;
wenzelm
parents: 28019
diff changeset
    14
  val get_int: T -> string -> int option
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    15
  val put: string * string -> T -> T
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    16
  val remove: string -> T -> T
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    17
end;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    18
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    19
structure Properties: PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    20
struct
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    21
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    22
type property = string * string;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    23
type T = property list;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    24
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    25
fun defined (props: T) name = AList.defined (op =) props name;
28032
cb0021c989cd added get_int;
wenzelm
parents: 28019
diff changeset
    26
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    27
fun get (props: T) name = AList.lookup (op =) props name;
28032
cb0021c989cd added get_int;
wenzelm
parents: 28019
diff changeset
    28
fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
cb0021c989cd added get_int;
wenzelm
parents: 28019
diff changeset
    29
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    30
fun put prop (props: T) = AList.update (op =) prop props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    31
fun remove name (props: T) = AList.delete (op =) name props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    32
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    33
end;