--- a/src/HOL/Tools/try0.ML Sun Apr 06 18:12:53 2025 +0200
+++ b/src/HOL/Tools/try0.ML Mon Apr 07 08:39:10 2025 +0200
@@ -30,6 +30,7 @@
val get_all_proof_method_names : unit -> string list
val schedule : string Config.T
+ val get_schedule : Proof.context -> string list list
datatype mode = Auto_Try | Try | Normal
val generic_try0 : mode -> Time.time option -> facts -> Proof.state ->
@@ -118,6 +119,20 @@
val schedule = Attrib.setup_config_string \<^binding>\<open>try0_schedule\<close> (K "")
+fun get_schedule (ctxt : Proof.context) : string list list =
+ let
+ fun some_nonempty_string sub =
+ if Substring.isEmpty sub then
+ NONE
+ else
+ SOME (Substring.string sub)
+ in
+ Config.get ctxt schedule
+ |> Substring.full
+ |> Substring.tokens (fn c => c = #"|")
+ |> map (map_filter some_nonempty_string o Substring.tokens Char.isSpace)
+ end
+
local
fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
@@ -175,16 +190,7 @@
fun generic_try0 mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state) =
let
- fun some_nonempty_string sub =
- if Substring.isEmpty sub then
- NONE
- else
- SOME (Substring.string sub)
- val schedule =
- Config.get (Proof.context_of st) schedule
- |> Substring.full
- |> Substring.tokens (fn c => c = #"|")
- |> map (map_filter some_nonempty_string o Substring.tokens Char.isSpace)
+ val schedule = get_schedule (Proof.context_of st)
fun iterate [] = ((false, (noneN, [])), [])
| iterate (proof_methods :: proof_methodss) =
(case generic_try0_step mode timeout_opt facts st proof_methods of