[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some

[Makarius]

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 
here?


 	Makarius