#732 Disappearing proof obligations in Explorer

[Laurent Voisin]

Sometimes, the Event-B Explorer view loses all the POs of a component and just displays a green node labelled "Proof Obligations" with no child. The statistics are also wrong (not counting the POs of the component). This seems to be caused by a concurrency bug when updating the model of the Event-B Explorer.

This bug has been hanging around for a long time. A partial fix was expected from commit [ba03c6], but was not complete as this bug still happens in Rodin 3.1 (as reported by Michael Leuschel in a private mail).

In retrospect, it seems that the only way to really get rid of this bug is to rework completely the handling of concurrency when maintaining the model of the Event-B Explorer.