src/Pure/General/properties.ML
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 46830 224d01fec36d
child 50842 777c6026ca93
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
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
    Author:     Makarius
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     3
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     4
Property lists.
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     5
*)
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     6
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     7
signature PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
     8
sig
46830
224d01fec36d tuned signature;
wenzelm
parents: 46829
diff changeset
     9
  type T = (string * string) list
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    10
  val defined: T -> string -> bool
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    11
  val get: T -> string -> string option
46830
224d01fec36d tuned signature;
wenzelm
parents: 46829
diff changeset
    12
  val put: string * string -> T -> T
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    13
  val remove: string -> T -> T
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    14
end;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    15
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    16
structure Properties: PROPERTIES =
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    17
struct
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    18
46830
224d01fec36d tuned signature;
wenzelm
parents: 46829
diff changeset
    19
type T = (string * string) list;
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    20
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    21
fun defined (props: T) name = AList.defined (op =) props name;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    22
fun get (props: T) name = AList.lookup (op =) props name;
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 29606
diff changeset
    23
fun put entry (props: T) = AList.update (op =) entry props;
28019
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    24
fun remove name (props: T) = AList.delete (op =) name props;
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    25
359764333bf4 Property lists.
wenzelm
parents:
diff changeset
    26
end;