Re: Remove IsaCoSy's builtin-in timeout

[Chris Warburton]

Looking for "timeout" in the isaplanner output directory, we also find
"timelimit" and some potential other avenues.

It looks like isabelle_dir/src/Pure/Concurrent/time_limit.ML defines a
"timeLimit" function which throws a "TimeOut" exception. This exception
gives rise to the "Timeout" error message, via a mapping in
isabelle_dir/src/Pure/Isar/runtime.ML

It looks lime some external tools are time-limited (e.g. Sledgehammer,
SMT and ATP solvers, E, Nitpick, quickcheck, etc.).

It looks like quickcheck might be of particular relevance, given that it
litters the IsaCoSy output. However, it looks like it's being invoked by
isabelle_dir/contrib/IsaPlanner/src/cinfos/counterex_cinfo.ML which is
handling the exception (returning a "NONE" result).