Proof Skeleton Design: Difference between revisions
imported>Nicolas New page: This document aims at helping developers getting into the code of the proof skeleton viewer. ==Purpose== The Proof Skeleton View gives the user the ability to quickly browse the skeleton... |
imported>Mathieu m Category:Design + use of class and method templates |
||
| Line 7: | Line 7: | ||
==Building the skeleton== | ==Building the skeleton== | ||
Core functions consist in rebuilding a proof tree from a saved proof. This is done in the | Core functions consist in rebuilding a proof tree from a saved proof. This is done in the {{class|ProofSkeletonBuilder}} class. | ||
Firstly, being given a proof, the root sequent can be built, using saved proof dependencies. | Firstly, being given a proof, the root sequent can be built, using saved proof dependencies. | ||
From that, the | From that, the {{class|ProofBuilder}} provides a {{method|reuse()}} method that allows reconstructing the proof tree from saved proof skeleton. | ||
==View architecture== | ==View architecture== | ||
The two-part view is based on Eclipse's form | The two-part view is based on Eclipse's form {{class|MasterDetailsBlock}}. The main idea is that the master part (on the left) contains browsable data (for us, a proof tree), and depending on the master element being selected (a rule in our case), the details part (on the right) is refreshed with data concerning this very element (sequents here). | ||
Classes are structured in the following way: | Classes are structured in the following way: | ||
| Line 24: | Line 24: | ||
DetailsPageProvider : returns the sequent details page when a proof tree node is selected | DetailsPageProvider : returns the sequent details page when a proof tree node is selected | ||
DetailsPage : contains a list viewer that displays the sequent of the currently selected node | DetailsPage : contains a list viewer that displays the sequent of the currently selected node | ||
[[Category:Design]] | |||
Revision as of 13:10, 12 December 2008
This document aims at helping developers getting into the code of the proof skeleton viewer.
Purpose
The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a convenient way to display rules and sequents together in the same view.
Building the skeleton
Core functions consist in rebuilding a proof tree from a saved proof. This is done in the ProofSkeletonBuilder class.
Firstly, being given a proof, the root sequent can be built, using saved proof dependencies. From that, the ProofBuilder provides a reuse() method that allows reconstructing the proof tree from saved proof skeleton.
View architecture
The two-part view is based on Eclipse's form MasterDetailsBlock. The main idea is that the master part (on the left) contains browsable data (for us, a proof tree), and depending on the master element being selected (a rule in our case), the details part (on the right) is refreshed with data concerning this very element (sequents here).
Classes are structured in the following way:
MasterDetailsBlock : creates the MasterPart and registers the DetailsPageProvider
MasterPart : contains the tree viewer and fires tree selection change events
ContentProvider : provides proof skeleton data to the tree viewer
LabelProvider : provides node labels and images to the tree viewer
DetailsPageProvider : returns the sequent details page when a proof tree node is selected
DetailsPage : contains a list viewer that displays the sequent of the currently selected node
