[Polyml] InterruptState

I realised that I was completely misunderstanding the use of the term “synchronous” in the description of the type InterruptState. I now believe that synchronous interrupts require co-operation from the thread being interrupted while asynchronous interrupts are pre-emptive (not the other way round). Have I got it right now?

The documentation says that asynchronous interrupts occur "at a suitable point soon after they are triggered”. Is iit possible to state what the suitable points are.

In any case, I think that my code (which is just trying to make a a call of a single-threaded function time out) should loop after sending the sending the interrupt waiting for the interrupted thread to become inactive. Does that sound right?

Regards,

Rob.