--- a/src/Pure/General/properties.ML Sat Dec 07 21:49:05 2024 +0100
+++ b/src/Pure/General/properties.ML Sat Dec 07 23:08:51 2024 +0100
@@ -18,6 +18,7 @@
val make_string: string -> string -> T
val make_int: string -> int -> T
val get_string: T -> string -> string
+ val get_bool: T -> string -> bool
val get_int: T -> string -> int
val get_seconds: T -> string -> Time.time
end;
@@ -44,6 +45,11 @@
val get_string = the_default "" oo get;
+fun get_bool props name =
+ (case get props name of
+ NONE => false
+ | SOME s => Value.parse_bool s);
+
fun get_int props name =
(case get props name of
NONE => 0