Rodin Platform 1.3 Release Notes: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Pascal |
imported>Tommy |
||
| Line 2: | Line 2: | ||
== What's New in Rodin 1.3? == | == What's New in Rodin 1.3? == | ||
* Event-B Editor | |||
:'''New in component popup menu'''. "New Event-B Project" and "New Event-B Component" wizards have been added to the "New" context menu of the event-B explorer. Right-clicking in a blank part or on a project in the Event-B explorer, a popup appears; then in the "New" section, these two actions are proposed. | |||
:'''new preference/properties mechanism'''. A new preference/properties mechanism to handle and use prefix settings. It is now possible to set prefixes for a workspace scope or a project scope. Prefix settings are extended automatically by editor contributions. | |||
:See also: [[Customize Prefixes]] | |||
* Proving Perspective | |||
:'''A new "Replay Proof" command'''. Right-clicking any element in the Event-B Explorer shows the contextual menu, which contains a new command "Proof Replay on Undischarged POs" next to "Retry Auto Provers" and "Recalculate Auto Status". | |||
:See also: [[Proof Obligation Commands]] | |||
:'''NewPP'''. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover". | |||
* Rodin Builder | |||
:'''Direct children processing only'''. The builder now only processes direct children of project. Files located in subfolders are ignored. | |||
* Changes for plugin-developers | |||
:'''Added the origin of predicates in a proof'''. In the sequent of the root node of a IProofTree, the IAxiom, IInvariant, ..., a predicate (hypothesis or goal) comes from can be fetched through the origin of its source location. | |||
:For instance: proofTree.getRoot().getSequent().goal().getSourceLocation().getOrigin() | |||
:'''Knowing nature of proof obligations'''. The nature of a proof obligation (Theorem, Well-Definedness, Invariant Preservation, ...) can be known from a IPOSequent. | |||
:See IPOGNature and IPOSequent#getPOGNature(). | |||
:'''NewPP Plug-in'''. The newPP tactic has been published. See PPCore#newPP() | |||
:'''Added ExplorerPlugin#getSelectedStatuses()'''. Added a function ExplorerPlugin#getSelectedStatuses() to get the PS elements under the current explorer selection. | |||
:'''Extensible pretty print'''. It is now possible to extend the pretty print page with the same kind of mechanism used to extend the structured editor. | |||
:See also: [[Extending the Pretty Print Page]] | |||
== Requirements == | == Requirements == | ||
Revision as of 08:37, 21 April 2010
What's New in Rodin 1.3?
- Event-B Editor
- New in component popup menu. "New Event-B Project" and "New Event-B Component" wizards have been added to the "New" context menu of the event-B explorer. Right-clicking in a blank part or on a project in the Event-B explorer, a popup appears; then in the "New" section, these two actions are proposed.
- new preference/properties mechanism. A new preference/properties mechanism to handle and use prefix settings. It is now possible to set prefixes for a workspace scope or a project scope. Prefix settings are extended automatically by editor contributions.
- See also: Customize Prefixes
- Proving Perspective
- A new "Replay Proof" command. Right-clicking any element in the Event-B Explorer shows the contextual menu, which contains a new command "Proof Replay on Undischarged POs" next to "Retry Auto Provers" and "Recalculate Auto Status".
- See also: Proof Obligation Commands
- NewPP. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover".
- Rodin Builder
- Direct children processing only. The builder now only processes direct children of project. Files located in subfolders are ignored.
- Changes for plugin-developers
- Added the origin of predicates in a proof. In the sequent of the root node of a IProofTree, the IAxiom, IInvariant, ..., a predicate (hypothesis or goal) comes from can be fetched through the origin of its source location.
- For instance: proofTree.getRoot().getSequent().goal().getSourceLocation().getOrigin()
- Knowing nature of proof obligations. The nature of a proof obligation (Theorem, Well-Definedness, Invariant Preservation, ...) can be known from a IPOSequent.
- See IPOGNature and IPOSequent#getPOGNature().
- NewPP Plug-in. The newPP tactic has been published. See PPCore#newPP()
- Added ExplorerPlugin#getSelectedStatuses(). Added a function ExplorerPlugin#getSelectedStatuses() to get the PS elements under the current explorer selection.
- Extensible pretty print. It is now possible to extend the pretty print page with the same kind of mechanism used to extend the structured editor.
- See also: Extending the Pretty Print Page
Requirements
TODO: Inform here of some specific system requirements (version of Java, etc).
External plug-ins
TODO: Describe here the available plug-ins, and the supported versions for this release.
Downloading
TODO: Add here a link to download the platform.
Fixed Bugs
TODO: Add here a list of the fixed bugs.
Known Issues
TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.3).
