diff -r 871caa4b3142 -r 8dc9453889ca src/Pure/General/properties.ML --- 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