equal
deleted
inserted
replaced
6 |
6 |
7 signature PROPERTIES = |
7 signature PROPERTIES = |
8 sig |
8 sig |
9 type entry = string * string |
9 type entry = string * string |
10 type T = entry list |
10 type T = entry list |
|
11 val entry_ord: entry ord |
|
12 val ord: T ord |
11 val defined: T -> string -> bool |
13 val defined: T -> string -> bool |
12 val get: T -> string -> string option |
14 val get: T -> string -> string option |
13 val put: entry -> T -> T |
15 val put: entry -> T -> T |
14 val remove: string -> T -> T |
16 val remove: string -> T -> T |
15 val seconds: T -> string -> Time.time |
17 val seconds: T -> string -> Time.time |
19 struct |
21 struct |
20 |
22 |
21 type entry = string * string; |
23 type entry = string * string; |
22 type T = entry list; |
24 type T = entry list; |
23 |
25 |
|
26 val entry_ord = prod_ord string_ord string_ord; |
|
27 val ord = list_ord entry_ord; |
|
28 |
24 fun defined (props: T) name = AList.defined (op =) props name; |
29 fun defined (props: T) name = AList.defined (op =) props name; |
25 fun get (props: T) name = AList.lookup (op =) props name; |
30 fun get (props: T) name = AList.lookup (op =) props name; |
26 fun put entry (props: T) = AList.update (op =) entry props; |
31 fun put entry (props: T) = AList.update (op =) entry props; |
27 fun remove name (props: T) = AList.delete (op =) name props; |
32 fun remove name (props: T) = AList.delete (op =) name props; |
28 |
33 |