New scheme for editing where display creates objects and informs prover of object deletions
Maybe less efficient for "lazy displays"
Something else:
Can we have a meaningful static notion of document here, perhaps by moving object attributes into the script markup (or metainfo elements inside thereof)?