TWiki> PG Web>ProofGeneralIssues >PGRevertReload (revision 1)EditAttach
Suggested by David in a mail from 13 May 06:
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
    | delobj+            # objects have been deleted
    | replaceobjs        # objects are being replaced
    | objectstate+        # objects have changed state

obj = element obj {
            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

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 26 Sep 2006 - 20:43:57 - ChristophLueth
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies