Discarding changes: revert/reload file. Actually what I want here is to revert to the Broker's in-memory version, by causing it to simply dump all of the objects again. (Maybe we also want the separate facility of reverting to the on-disk file, although we can already achieve that by followed by again, which seems OK).

  reloadobjs = element reloadobjs { proverid_attr, srcid_attr }

(not sure if we need the proverid_attr or not: it's included in some of the dispobjcmds but not all).

The reloadobjs could optionally take a modtick_attr to implement a version for undo/redo target. Seems easy at least in terms of edit contents, prover synchronisation would be harder of course.

Answered by Christoph 16 May 06:

I think that needs a new display message, because at the moment the broker can only announce new objects. So to keep in the current framework, we'd need a replaceobjs message or some such. Suggestion: we extend dispobjmsg to allow an "obj" message which reports existing objects

dispobjmsg = element dispobjmsg {
      newobj+            # new objects have been created
    | obj+                      # broker reports existing object in response to
reloadobjs
    | delobj+            # objects have been deleted
    | replaceobjs        # objects are being replaced
    | objectstate+        # objects have changed state
    }

obj = element obj {
        proverid_attr,
            srcid_attr,
        objid_attr,
            attribute objposition { objid } ?,
            objtype_attr ?,
            attribute objparent { objid }?,
            attribute objstate { objstate },
            (properscriptcmd | unparseable) }

or alternatively, adding an attribute to the newobj message.

On rereading this, I wonder why the broker could not just rebroadcast all objects in the file in question with a newobj message. (This may cause problems if there is more than one display connected, of course.)

Status: unresolved.

-- ChristophLueth - 26 Sep 2006