PGRevertReload < PG

PG Web>ProofGeneralKit>PGKitDevelopment>KitDevelIssues>PGRevertReload (28 Sep 2006, ChristophLueth) (raw view)EditAttach

Suggested by David in a mail from 13 May 06:
<blockquote>
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 <discardfile>
followed by <dispopenfile> again, which seems OK).

<pre>
  reloadobjs = element reloadobjs { proverid_attr, srcid_attr }
</pre>

(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.
</blockquote>

Answered by Christoph 16 May 06:
<blockquote>
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

<pre>
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) }
</pre>
or alternatively, adding an attribute to the newobj message.
</blockquote>

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: see request for change PGNewObjMessages

-- Main.ChristophLueth - 26 Sep 2006

Topic revision: r3 - 28 Sep 2006 - 23:20:39 - ChristophLueth

Copyright © 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