fix(web): fix push message race condition

In some resource-constrained environments (e.g., my VPS with 2 vCPUs),
it was possible for validation and highlighting precomputation to be
finished before the server responded to a deltaText updating completion
request (updating completion take longer than a normal update, because
they also have to compute the completions). Therefore, the client
received push messages about a stateId it didn't know about yet.

To fix this, we delay any push messages originating during servicing a
call to be sent after the call is serviced. Thus the client first
receives the updating completion response with the new stateId, followed
by the push messages relating to that stateId.

0 files changed, 0 insertions, 0 deletions