Difference between pages "Rodin Platform 1.3 Release Notes" and "File:FunOvrHypAfter1.png"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
(Maintenance script uploaded File:FunOvrHypAfter1.png)
 
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]]
 

Latest revision as of 20:50, 30 April 2020