Opened 17 years ago
Last modified 11 years ago
#54 new defect
Support file operations save-as, rename, revert properly during script management
| Reported by: | Owned by: | David Aspinall | |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
These file operations corrupt the synchronisation with the prover:
- Revert should retract the document if any changes overlap a processed region
- Save-As should switch to the new file, retracting the old, and possibly retracting any overwritten file.
The simplest thing to do --- if possible in Eclipse --- is to disable save-as/revert/renaming for the active script file, and to automatically retract files that are overwritten and locked.
Change History (2)
comment:1 Changed 17 years ago by
| Description: | modified (diff) |
|---|---|
| Summary: | File operation save-as and rename should track state change in scripting → Support file operations save-as, rename, revert properly during script management |
comment:2 Changed 11 years ago by
| Milestone: | PG-Eclipse-1.1.0 |
|---|
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted