src/Pure/General/properties.ML
changeset 81557 8dc9453889ca
parent 80504 7ea69c26524b
--- 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