Opened 17 years ago

Closed 16 years ago

Last modified 11 years ago

#7 closed enhancement (fixed)

Finish proof explorer: inherit decorators, menus, etc. from Project Explorer.

Reported by: anonymous Owned by: Graham Dutton
Priority: major Milestone:
Component: 1:pg-eclipse Keywords:
Cc:

Description (last modified by Graham Dutton)

The Proof Explorer view needs to inherit more of the functionality of the Project Explorer, including decoration and extra menus.

Change History (13)

comment:2 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from David Aspinall to anonymous
Status: newassigned

Platform menu contributions (open, etc) fixed in plugin.xml 1.131.

Still to do: label decorators for standard error markers. I'm not sure whether this should be provided by the platform or not. If not, the code should be easy to grab from another project.

comment:3 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from anonymous to David Aspinall
Status: assignednew

comment:4 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from David Aspinall to anonymous
Status: newassigned

comment:5 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from anonymous to David Aspinall
Status: assignednew

comment:6 Changed 17 years ago by Graham Dutton

Owner: changed from David Aspinall to anonymous

Note that error decoration system must be in place first! See ticket #71 for details.

comment:7 Changed 17 years ago by David Aspinall

Owner: changed from anonymous to David Aspinall
Type: defectenhancement

comment:8 Changed 17 years ago by David Aspinall

Owner: changed from David Aspinall to Graham Dutton

comment:9 Changed 17 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.6PG-Eclipse-1.0.7

comment:10 Changed 16 years ago by Graham Dutton

see also ticket #71

comment:11 Changed 16 years ago by Graham Dutton

Description: modified (diff)
Summary: Finish proof explorer: add decorators for errors and rest of menusFinish proof explorer: inherit decorators, menus, etc. from Project Explorer.

Updated for clarity. It's the Project Explorer which more closely reflects what we require.

comment:12 Changed 16 years ago by David Aspinall

Resolution: fixed
Status: newclosed

The content filter now works properly for the navigator, which was hiding files and folders inside projects. Now I've adjusted the filter, files and decorators, etc appear (see plugin.xml). I've also added further "new" wizards. Closing this for now as the navigator is now quite usable.

comment:13 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.7

Milestone PG-Eclipse-1.0.7 deleted

Note: See TracTickets for help on using tickets.