Ideas discussed:

  • 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)?

-- DavidAspinall - 18 Jul 2007


This topic: PG > PGIP > PGIPDevelNotes > SomeUseCasesForEditing > MoreThoughtsAboutDisplayProtocol
Topic revision: r1 - 18 Jul 2007 - 14:13:47 - DavidAspinall
 
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