--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Feb 15 08:36:19 2021 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Feb 19 11:52:34 2021 +0100
@@ -32,6 +32,7 @@
val theorems_of_sucessful_proof : Toplevel.state option -> thm list
val get_setting : (string * string) list -> string * string -> string
val get_int_setting : (string * string) list -> string * int -> int
+ val get_bool_setting : (string * string) list -> string * bool -> bool
val cpu_time : ('a -> 'b) -> 'a -> 'b * int
end
@@ -209,6 +210,12 @@
| SOME NONE => error ("bad option: " ^ key)
| NONE => default)
+fun get_bool_setting settings (key, default) =
+ (case Option.map Bool.fromString (AList.lookup (op =) settings key) of
+ SOME (SOME i) => i
+ | SOME NONE => error ("bad option: " ^ key)
+ | NONE => default)
+
fun cpu_time f x =
let val ({cpu, ...}, y) = Timing.timing f x
in (y, Time.toMilliseconds cpu) end