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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
