Opened 17 years ago
Last modified 11 years ago
#127 assigned defect
Fix Action Bar active editor switching; simplify actions — at Version 1
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
PG often loses track of the active editor. Instead of self managing this in our own way we should use the standard Eclipse mechanism for retargeted actions. It's slightly more complicated, but allows us to attach an action set to the script editor only and our own views.
Change History (1)
comment:1 Changed 17 years ago by
| Description: | modified (diff) |
|---|---|
| Priority: | critical → blocker |
| Summary: | Fix Action Bar active editor switching → Fix Action Bar active editor switching; simplify actions |
Note: See
TracTickets for help on using
tickets.
I've started work on this, at the same time simplifying the handling of actions to eliminate the common problems of "action is already running" and "someone else owns the prover". At the moment things are very broken!