equal
deleted
inserted
replaced
77 |
77 |
78 (* timeout *) |
78 (* timeout *) |
79 |
79 |
80 val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0) |
80 val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0) |
81 |
81 |
82 val time_of_timeout = Time.fromReal o Config.apply timeout |
82 val timeout_seconds = seconds o Config.apply timeout |
83 |
83 |
84 fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x |
84 fun with_timeout ctxt f x = Timeout.apply (timeout_seconds ctxt) f x |
85 |
85 |
86 |
86 |
87 (* extending the tactic *) |
87 (* extending the tactic *) |
88 |
88 |
89 type trans_context = |
89 type trans_context = |