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 are comments/whitespace, we do not have to prohibit the user from editing them (and we could tweak the colouring).
2. 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.
3. 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

Some comments on that:

• I agree that if we want that (colouring comments) the broker should do it. The reason the broker is that I thought it odd that comments have a state. It's also easier to implement this way. Not that I would ever cut corners, you understand.
• I agree with the second/third point as well. If we go with the philosophy of "make the broker smart not the interface", and if we think that the "stepping through" gestures of PGClassic are a good thing to have (I think so), we should make this primitive display commands, like

element movefocus { attribute ("back"|"forward"|"topoftheory" | "topoffile" | "endoftheory" | "endoffile" | "here") }

(here will probably need explicit arguments where "here" is). This allows display to easily bind these things to buttons, mouse gestures etc. without needing to be clever.

If we agree on the syntax, I'll put this on my ToDo list.

-- ChristophLueth - 02 Oct 2006

That sounds excellent! We straight away get easy actions for the standard navigation buttons and junk a bunch of messy code. The only one left with any work is here which needs to search for the nearest object before or after the point.

I don't mind much about the syntax and your names are better than the ones from PGClassic (which were: undo, next, retract, use, goto). What is useful is if names are followed in the code to avoid too much confusion --- but I can change the names of my buttons easily enough (and lucky Eclipse has refactoring to do this really easily).

File-oriented displays like Emacs and Eclipse will not use topoftheory or endoftheory but presumably desktop-oriented displays like PG Win would.

-- DavidAspinall - 02 Oct 2006