But I'm wondering what to do with asynchronous edits in the display that take place while we are waiting for the response to an request. And on a related issue, how to deal with prover- or broker- generated edits that might not be requested by the display.

Did you consider this with Ahsan? I wonder how the Eclipse mode solves this. (Also I suspect you and I may have talked about this or a similar race condition before).

To be clear the problem is when this happens:

  Display                                Broker

  user edits
  .      -------------------------->
  .                <editobj>
  more edits                             parse,etc
  .
  .
  .     <---------------------------
                   <dispobjmsg>

The "more edits" in the display may occur inside objects replaced by the replaceobjs in dispobjmsg, for example. In a bit of testing with the automatic parsing, I think I noticed this happening once: some text I'd just written vanished! It's a bit tricky to trigger because the broker responds quickly and the editobjs are sent after a full second of idle time, so you need to type at just the right moment. (Even harder to trigger with the manual reparse).

The simplest thing to do is to prevent "more edits" from occuring by blocking in the display. That maybe doesn't have a too bad behaviour at the moment playing with small files, small edits and quick parsers, but it probably isn't ideal.

Otherwise to be more flexible I think we need to provide resolution either Display-side or Broker-side:

1. Display replay.

The display keeps history of "more edits" and (optionally) the buffer contents before they occur, i.e. checkpointing when is sent. When "replaceobjs" arrives, it retracts the edits (restoring the object boundaries), commits the replaceobjs and then replays the edits. We expect the replay to work because the replaceobjs doesn't change the buffer contents, only object information. The edits might have slightly different behaviour because of changes in object status, but this should only amount to whether a region turns underlined/red or not.

2. Broker roll-back.

The broker keeps a history of the object layout and contents before is processed. After a is sent to the display, it waits for an acknowledgement in a new message to indicate whether the edit succeeded or not. If the edit did not succeed, it rolls back the object layout to the previous state.

     <----------------------------------
           <dispobjmsg>
     ----------------------------------->
           <editresult accept="true"/>

Now (you guessed it) I think the Broker-based solution is better. First, because the Broker is going to be better at managing this (it would be a tricky hack in Emacs) and in general our philosophy is that it's better to solve things once in the Broker than many times, in each display. And second, this mechanism seems to extend well to edits which are not requested by the display (perhaps coming from another display, the broker or the prover). At the moment if those arrive and conflict with the current display we have no way to resolve them (and we might not even notice the conflict).

If the replacement is as a result of a request from this display, then the display can choose to accept the edit or not. If the replacement is a request from elsewhere, it may conflict with what the user has edited locally (we can tell this by comparing the regions affected by local edits and replaceobjs). We can then recover in the display by asking if the user wants to discard his changes or not --- but the display should report the edit result as accepted, I think. (The broker must thus send an replaceobjs to the requesting display, if any, first; wait to see if it is accepted there, and then only after try to propagate it to other displays if it is accepted).

I'm not looking for fully-fledged transaction handling here, I think it's reasonable to restrict displays to having at most one editobj request outstanding. On the other hand, if we have multiple displays making edits, there can be races between them which must be resolved by the broker. (E.g. the broker commits to the first edit it receives and which is accepted back successfully, it then sends with an attribute to indicate that that the result is an edit from elsewhere and must be accepted.)

What do you think?

Unfortunately it is an incompatible change because of the extra message (although this is only needed in case the display "owns" the edit/file and wants the chance to refuse edits). We could either try to get that implemented in Eclipse quickly, or put in a backwards compatibility hack of some form.

Perhaps for now we should think about the distributed editing model a bit more carefully before deciding what to do. In the meantime, there are a couple of small improvements which I think might help in any case, I'll write about them in another message.

The rather noncommital answer from Christoph from 15 may 06 is excerpted here for historical authenticitiy:

So, the present situation is that in a situation as you describe, the broker will discard the edits made after an editobj message has been sent, and before the dispobjmsg is sent. This is what you observed, and I think this is also how the Eclipse mode behaves. (It may even lock, not sure.)

[...] My gut feeling is that we have to be careful here not to open a huge can of complications (locking is simple and might not be that bad), but I can't pin down anything which is wrong with your suggestion.

Clearly, the issue is far from resolved :-}

-- ChristophLueth - 26 Sep 2006