discontinued unused / untested distinction of separate PIDE modules;

proper signaling after each state update (NB: ML version does this uniformly via timed_access);

synchronized access, similar to ML version;

tuned signature in accordance to ML version;

more uniform synchronized variables;