[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some
makarius at sketis.net
Mon Jul 25 10:22:07 CEST 2011
On Sun, 24 Jul 2011, Lukas Bulwahn wrote:
>> In Isabelle/318ca53e3fbb it works half-way, when the outer execution
>> context is not a worker task itself, e.g. on the tty.
> For tool developers, this means as consequence, we either do not use
> Par_List.get_some or ensure by other means, that we know if the outer
> execution context is a worker task or not, when being invoked, right?
You cannot really ensure a non-worker context in reality. This is merely
a hint that experiments can be done on the raw tty at the moment.
Of course I will revisit the issue again and more thoroughly, when I am
back from travel in 2 weeks.
> Eventually, this context-sensitive behaviour implemented above can then
> be removed if nested Par_List operations are allowed.
Par_List is just a thin wrapper for the Future library, and it all should
be nestable in the same way. Did you experience any further problems
More information about the isabelle-dev