RodinCore Log


Commit Date  
[0e84d7] by Nicolas Beauger Nicolas Beauger

Require an icon for dynamic dropdown tactic extensions.

Add an icon to the extension for 'Profiles' dropdown.

There used to be only a name, but since we switched to Eclipse 3.8, on linux and windows platforms, the dropdown tool items have space for an image on top of the text, even when no image is set. This make the whole Proof Control toolbar take more vertical space, with dropdown buttons expanding vertically, which is annoying, aesthetically, but most especially because of space loss.
Thus, we now only display the icon, the name is stored but not used for now (like UI tactics in the same extension point).

2014-03-13 15:52:03 Tree
[dfadcf] (RodinCore/3.0RC2) by Nicolas Beauger Nicolas Beauger

Restore replacer for product version

Affects @version@ in branding plug-in properties.
The better mechanism used with tycho 0.19 does not work with tycho 0.18.2.
But version 0.19 breaks update site configuration !
Restores commit be7acfe6cf, which modifies the working copy.

2014-02-24 13:26:07 Tree
[4ea65b] by Nicolas Beauger Nicolas Beauger

Restore end of line in property file

2014-02-24 13:13:37 Tree
[c6668f] by Laurent Voisin Laurent Voisin

Revert to Tycho 0.18.1

With Tycho 0.19.0, the p2.inf of the branding plug-in of the platform
gets lost and therefore no update site is available in the product.

2014-02-21 17:44:09 Tree
[3b552e] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Rename to FreshInstantiation, adding missing 'i'

2014-02-21 11:16:59 Tree
[5f17df] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Add a utility method to generate fresh free identifiers

Use this new method in reasoners that introduce fresh free identifiers.

2014-02-21 11:13:16 Tree
[7a21dd] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Remove FIXME in TrivialRewriter about bound identifier name

The bound identifier name has no more risk of collision,
as it is solved when printing or freeing.

2014-02-21 11:11:31 Tree
[29d360] by Nicolas Beauger Nicolas Beauger

Add tests about explicit ubiquitous relationship

2014-02-21 10:03:43 Tree
[90a30b] by Nicolas Beauger Nicolas Beauger

Add tests about ubiquitous elements and attributes

2014-02-17 16:56:19 Tree
[ddb152] by Nicolas Beauger Nicolas Beauger

Add method isUbiquitous() to element types and attribute types

2014-02-17 15:24:28 Tree
[6af29c] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Use ubiquitous extension to define "generated" attribute relationship

2014-02-13 17:52:15 Tree
[68b117] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Add support for ubiquitous items from item types

Add API to the ElementTypeManager to retrieve ubiquitous items.
Integrate ubiquitous items in the database relationship API.

2014-02-13 17:44:50 Tree
[e6462e] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Computes ubiquitous elements for further use

Ubiquitous relations are traversed and ubiquitous items are stored so
that the element type manager can further retrieve them.

2014-02-13 17:10:48 Tree
[23d673] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Add the ubiquitous parser as sub parser of item relations parser

2014-02-13 15:41:14 Tree
[6e9807] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Create ubiquitous relation object and its dedicated parser

2014-02-13 15:24:05 Tree
[86f749] by Thomas Muller Thomas Muller , pushed by Nicolas Beauger Nicolas Beauger

Add ubiquitous element in the itemRelations extension point

This element defines child or attribute relationships defined globally
for any internal element.

2014-02-13 13:37:47 Tree
[f59453] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Add a combine() method with name and description

The resulting combined tactic returned by ICombinatorDescriptor
used to bear the name and description of the combinator,
which was not relevant for client defined tactics.
It occurred in particular for dynamic tactics, with for instance
'Loop On All Pending' as a tactic name.
Clients can now provide a meaningful name and a description.

2014-01-23 16:44:09 Tree
[e0277f] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Introduce dynamic tactic references to handle dynamic tactics

Dynamic tactics used to be serialized in extension. Thus, the origin of
the dynamic tactic was completely lost once used in a profile, and the
tactic that was applied was the serialized one, which was not the
intended behaviour for dynamic tactics.

Add the IDynamicTacticRef interface, returned by the auto tactic
registry, that contains the id, name and description of a dynamic
tactic. Instances of this interface are serialized as dynamic tactics,
with the dynamic tactic id alone (instead of the expanded tactic with
combinators, etc).

With this mechanism, dynamic tactic instances are computed when calling
ITacticDescriptor#getTacticInstance(), so as to obtain a fresh instance
from the dynamic tactic provider.

Remove method getDynTactics() which was freezing the tactics at call
time instead of implementing late binding.

2014-01-23 14:39:34 Tree
[d857dd] by Laurent Voisin Laurent Voisin

Revisit failing AST tests

Extract two failing tests that are now working.

Document better the remaining two.

2014-02-20 15:07:17 Tree
[c9bfd9] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Fix form of quantified expressions

The form used to remain implicit when the expression did not contain all
quantified identifiers, or when it contained externally bound identifiers.
The form filter now performs these additional checks, and switches to
explicit form when they are not fulfilled.

Add corresponding tests.

Fix test quantifiedExpression_LambdaToImplicit which was wrong.

2014-02-10 15:04:37 Tree
[f987dc] by Laurent Voisin Laurent Voisin

Remove unneeded qualification

Constants delcared in super class are directly visible.

2014-02-20 14:42:15 Tree
[efd7d0] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Remove warning about Unloadable class in core tests

Move Unloadable class used for POG tests in the 'tool' package.
Use it for both SC and POG loading tests.

2014-02-20 15:10:36 Tree
[3348bc] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Add API problem filter about non API class Module

2014-02-14 10:22:51 Tree
[ae429f] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Publish IState

Also add problem filters for methods that mention it.
ALso get rid of org/eventb/internal/core/tool/types/ package.

2014-02-13 16:37:30 Tree
[a6ea52] by Nicolas Beauger Nicolas Beauger , pushed by Laurent Voisin Laurent Voisin

Publish IFilterModule, IModule and IProcessorModule.

Also add problem filters to already published methods that returned these formerly non-API types.

2014-02-13 16:19:12 Tree
Older >

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks