Difference between revisions of "Proof Purger Interface"

From Event-B
Jump to navigationJump to search
imported>Mathieu
imported>Mathieu
m (Use some typesetting template)
Line 5: Line 5:
 
==Selecting purge input==
 
==Selecting purge input==
  
In any view, right-clicking an Event-B project or file will display a popup menu, containing a "Purge Proofs..." item.
+
In any view, right-clicking an Event-B project or file will display a popup menu, containing a {{menu|Purge Proofs...}} item.
 
If several files or projects (or both) are selected, purging will apply to all of them.
 
If several files or projects (or both) are selected, purging will apply to all of them.
  
Line 18: Line 18:
 
For the moment, nothing has been erased. The new window shows unused proofs and offers to choose among them which ones should be deleted. One may wish to keep some of them, knowing they might be useful in the future.
 
For the moment, nothing has been erased. The new window shows unused proofs and offers to choose among them which ones should be deleted. One may wish to keep some of them, knowing they might be useful in the future.
  
Once the selection has been decided, clicking the "Delete" button will actually delete selected proofs from proof files.
+
Once the selection has been decided, clicking the {{button|Delete}} button will actually delete selected proofs from proof files.
 
Files becoming empty will be deleted as well.
 
Files becoming empty will be deleted as well.
  
 
[[Category:User documentation]]
 
[[Category:User documentation]]

Revision as of 21:55, 11 December 2008

Purpose

Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to allow the user to get rid of these proofs.

Selecting purge input

In any view, right-clicking an Event-B project or file will display a popup menu, containing a Purge Proofs... item. If several files or projects (or both) are selected, purging will apply to all of them.

Firstly, the proof purger tries to find unused proofs in the selection. If none are found, a message will appear telling that no proof needs to be purged. Else, a new window will show the result.

Choosing proofs to delete

SelectProofsToDelete.jpg

For the moment, nothing has been erased. The new window shows unused proofs and offers to choose among them which ones should be deleted. One may wish to keep some of them, knowing they might be useful in the future.

Once the selection has been decided, clicking the Delete button will actually delete selected proofs from proof files. Files becoming empty will be deleted as well.