imported>Tommy |
|
Line 1: |
Line 1: |
− | {{TOCright}}
| |
| | | |
− | == 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).}}
| |
− |
| |
− | [[Category:Rodin Platform Release Notes]]
| |