Management of objects by displays -- can it be made easier?

Here are some thoughts about some possible protocol/broker changes prompted by writing Emacs display (notes from May '06):

  1. Object status for comments/whitespace: It's a hassle for the display to search through buffer for next object to undo/do. The only reason this is necessary is because of whitespace/comment objects. Perhaps the broker could simply fake the status changes for these objects?
    This might give a neater appearance too, familiar from the existing Proof General mode (whole buffer gets coloured, not just non-comments).
    Since we know the elements comments/whitespace, we do not have to prohibit the user from editing them (and we could tweak the colouring).

  1. Additionally/alternatively: it would be handy if the broker could indicate the next object to be processed/unprocessed in some intelligent order. The intelligent order could come by default from the order in the file (linear dependency), otherwise from the order given by a previous proof execution and dependency information.

  1. Actually: with non-linear dependency it seems hard for the display to make a simple request to "do all" or "undo all" the whole buffer contents (unless we assume that buffer must begin/end with a single owning theory declaration).

-- DavidAspinall - 01 Oct 2006

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 01 Oct 2006 - 10:54:28 - 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