author | wenzelm |
Mon, 30 May 2022 10:52:00 +0200 | |
changeset 75489 | f08fd5048df3 |
parent 71465 | 910a081cca74 |
child 77772 | 7e0d920b4e6e |
permissions | -rw-r--r-- |
28019 | 1 |
(* Title: Pure/General/properties.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Property lists. |
|
5 |
*) |
|
6 |
||
7 |
signature PROPERTIES = |
|
8 |
sig |
|
50842 | 9 |
type entry = string * string |
10 |
type T = entry list |
|
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
11 |
val entry_ord: entry ord |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
12 |
val ord: T ord |
28019 | 13 |
val defined: T -> string -> bool |
14 |
val get: T -> string -> string option |
|
50842 | 15 |
val put: entry -> T -> T |
28019 | 16 |
val remove: string -> T -> T |
51665 | 17 |
val seconds: T -> string -> Time.time |
28019 | 18 |
end; |
19 |
||
20 |
structure Properties: PROPERTIES = |
|
21 |
struct |
|
22 |
||
50842 | 23 |
type entry = string * string; |
24 |
type T = entry list; |
|
28019 | 25 |
|
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
26 |
val entry_ord = prod_ord string_ord string_ord; |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
27 |
val ord = list_ord entry_ord; |
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
51665
diff
changeset
|
28 |
|
28019 | 29 |
fun defined (props: T) name = AList.defined (op =) props name; |
30 |
fun get (props: T) name = AList.lookup (op =) props name; |
|
43780 | 31 |
fun put entry (props: T) = AList.update (op =) entry props; |
28019 | 32 |
fun remove name (props: T) = AList.delete (op =) name props; |
33 |
||
51665 | 34 |
fun seconds props name = |
35 |
(case AList.lookup (op =) props name of |
|
36 |
NONE => Time.zeroTime |
|
37 |
| SOME s => Time.fromReal (the_default 0.0 (Real.fromString s))); |
|
38 |
||
28019 | 39 |
end; |