RODIN

Revision: 7067
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7067&view=rev
Author:   nicolas_beauger
Date:     2009-04-24 15:39:23 +0000 (Fri, 24 Apr 2009)

Log Message:
-----------
Adapted to mathematical language V2.
Implemented a formula upgrader towards V2.
Changed context, machine and proof files version numbers to upgrade formulas from V1 to V2.
Added the "PartitionRewrite" tactic to the default auto tactics.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCIdentifierElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/AssignmentIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ElementIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ExpressionIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/PredicateIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POMTacticPreference.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/AssignmentModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/ExpressionModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/IdentifierModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/PredicateModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/EventBTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextDependenciesTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/EventBIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/IntegrationTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineDependenciesTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pm/TestUserSupportChangeDeltas.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pm/TestUserSupportChanges.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineRefines.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/AutoPOMTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/POLoaderTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/POUtil.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/upgrade/
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/upgrade/UpgraderV1V2.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/versions/TestEventBVersion_004_M_002_C_001_P.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7086
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7086&view=rev
Author:   lvoisin
Date:     2009-05-06 09:39:59 +0000 (Wed, 06 May 2009)

Log Message:
-----------
Introduction of "theorems almost everywhere":
  - Deprecation of theorem elements
  - Introduction of theorem attribute.
  - Update of static checker and POG.
Guards have been prepared to carry the theorem attribute, but this attribute
must currently be false (checked by the SC).
This is joint work from Stefan Hallerstede and Nicolas Beauger.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IAction.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IAxiom.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ICarrierSet.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IConstant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IGuard.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IInvariant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCAxiom.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCGuard.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCInvariant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCTheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ITheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IWitness.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Action.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Axiom.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/CarrierSet.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Constant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Guard.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Invariant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/MachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCInternalContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCTheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Theorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Variable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Variant.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Witness.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/state/IPredicateTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/GraphProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/SCProcessorModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ContextIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/MachineIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/ContextAxiomModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/ContextHypothesesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventWitnessModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineHypothesesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineInvariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/GlobalHypothesesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/PredicateModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/TheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/symbolTable/SymbolFactory.java
    trunk/RodinCore/org.eventb.core.tests/plugin.xml
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/EventBTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/GenericContextTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/GenericEventTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/GenericMachineTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/IGenericElementTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextDependenciesTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/EventBIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/IntegrationTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineDependenciesTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/DeltaCheckingTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/GenericHintTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/GenericPredicateTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestAccuracy.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestDependencies.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineEventWitnesses.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineEvents.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineHints.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineInit.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineInvariantsAndTheorems.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineRefines.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineSeesContext.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineVariant.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestPOFilter.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/BasicSCTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/DeltaCheckingTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericContextSCTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericEventSCTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericIdentTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericMachineSCTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericPredicateTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GraphProblemTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/IGenericSCTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestAccuracy.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestAxiomsAndTheorems.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestConstants.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestDependency.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEventRefines.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEvents.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestInvariantsAndTheorems.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestMachineRefines.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestOptionalAttributes.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestSeesContext.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestVariables.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestVariant.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TypeEnvironmentTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/versions/EventBVersionTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/versions/TestEventBVersion_004_M_002_C_001_P.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IDerivedPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/ContextAxiomTheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineInvariantTheoremModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/versions/TestEventBVersion_003_C.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/versions/TestEventBVersion_005_M.java

Removed Paths:
-------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/state/IContextTheoremTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/state/IMachineTheoremTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/ContextTheoremTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/MachineTheoremTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/ContextTheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineTheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/PredicateToProveModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/TheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/ContextTheoremFreeIdentsModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/ContextTheoremModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineTheoremFreeIdentsModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineTheoremModule.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7087
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7087&view=rev
Author:   nicolas_beauger
Date:     2009-05-06 14:51:23 +0000 (Wed, 06 May 2009)

Log Message:
-----------
Fixed POG so that no PO is generated for derived invariant establishment or preservation.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/MachineEventInvariantModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineEvents.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7196
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7196&view=rev
Author:   nicolas_beauger
Date:     2009-05-29 14:41:40 +0000 (Fri, 29 May 2009)

Log Message:
-----------
Event-B Indexers: implemented new constraint:
declared names must not be empty.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ContextIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventBIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/IdentTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/MachineIndexer.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineIndexerTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7198
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7198&view=rev
Author:   carinepascal
Date:     2009-05-29 16:50:36 +0000 (Fri, 29 May 2009)

Log Message:
-----------
Fixed Bug #2724926:  No location for warning.
The warning location now highlights when double-clicking on the warning.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventRefinesModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEventRefines.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7199
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7199&view=rev
Author:   nicolas_beauger
Date:     2009-05-29 17:10:16 +0000 (Fri, 29 May 2009)

Log Message:
-----------
AutoCompletion: implemented the filtering of propositions for witness labels on deterministically assigned disappearing abstract variables.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/CompletionUtil.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7213
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7213&view=rev
Author:   carinepascal
Date:     2009-06-02 14:49:59 +0000 (Tue, 02 Jun 2009)

Log Message:
-----------
Fixed Bug #2798407:  Events can have an empty label.
The static checker now ensures that the labeled elements don't have an empty label.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/GraphProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/LabeledElementModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericPredicateTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GraphProblemTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEvents.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestVariant.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7215
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7215&view=rev
Author:   nicolas_beauger
Date:     2009-06-03 12:49:47 +0000 (Wed, 03 Jun 2009)

Log Message:
-----------
Autocompletion:
- added a prefix argument to filter the results with
- corrected the visibility of disappearing variables

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7218
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7218&view=rev
Author:   nicolas_beauger
Date:     2009-06-03 15:24:51 +0000 (Wed, 03 Jun 2009)

Log Message:
-----------
Autocompletion:
* got primed variables in a more tidy way
* returned seen events labels for an event label

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/CompletionUtil.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/IdentTable.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7243
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7243&view=rev
Author:   nicolas_beauger
Date:     2009-06-12 14:18:36 +0000 (Fri, 12 Jun 2009)

Log Message:
-----------
Fixed Bug 2804046: AssertionError in Indexer.
  - Fixed NPE in AST for isValidIdentifierName().
  - Improved check for identifiers

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ContextIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventBIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/MachineIndexer.java
    trunk/RodinCore/org.eventb.core.ast/src/org/eventb/core/ast/FormulaFactory.java
    trunk/RodinCore/org.eventb.core.ast/src/org/eventb/internal/core/parser/Scanner.java
    trunk/RodinCore/org.eventb.core.ast/src/org/eventb/internal/core/parser/bmath.lex
    trunk/RodinCore/org.eventb.core.ast.tests/src/org/eventb/core/ast/tests/TestLexer.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineIndexerTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7295
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7295&view=rev
Author:   nicolas_beauger
Date:     2009-06-29 13:24:19 +0000 (Mon, 29 Jun 2009)

Log Message:
-----------
Fixed bug #2813537: Error in POG (ArrayIndexOutOfBoundsException in AbstractEventActionTable)
Bad array initialization size.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/AbstractEventActionTable.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineInit.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7300
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7300&view=rev
Author:   lvoisin
Date:     2009-07-01 14:33:49 +0000 (Wed, 01 Jul 2009)

Log Message:
-----------
Added option Eclipse-ExtensibleAPI to manifest files for the AnimB plug-in.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core.ast/META-INF/MANIFEST.MF


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7301
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7301&view=rev
Author:   lvoisin
Date:     2009-07-01 14:36:30 +0000 (Wed, 01 Jul 2009)

Log Message:
-----------
Multiple configurations in event-B tools:
  - moved the patch for SC to the generic class so that it is now also used by the POG.
  - reverted the SC code to the previous version in SVN
  - added a test for multiple configurations.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/tool/ConfigManager.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/tool/SCModuleManager.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/ProjectBuildTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7359
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7359&view=rev
Author:   nicolas_beauger
Date:     2009-07-11 22:23:47 +0000 (Sat, 11 Jul 2009)

Log Message:
-----------
Indexers: implemented root element indexing

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ContextIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventBIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/MachineIndexer.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/BridgeStub.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/ContextIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineCancelTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/MachineIndexerTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/indexers/OccUtils.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/DependenceIndexer.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7439
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7439&view=rev
Author:   nicolas_beauger
Date:     2009-08-13 08:55:23 +0000 (Thu, 13 Aug 2009)

Log Message:
-----------
Implemented support for versioning reasoners.
Reasoners may now bear a version number that evolves along with their behaviour.
For instance, when correcting a bug in a reasoner, increasing its version number subsequently makes all proofs where the old reasoner version has been used unreuseable by the ProofBuilder (i.e a replay will be performed instead of a reuse for the proof rules that use the old reasoner).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBProofElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover/schema/reasoners.exsd
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerOutput.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerRegistry.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverFactory.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverLib.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/proofBuilder/ProofBuilder.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/Messages.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ReasonerOutput.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ReasonerRegistry.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/messages.properties
    trunk/RodinCore/org.eventb.core.seqprover.tests/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/ProofBuilderTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/reasonerExtentionTests/AbstractReasonerTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/reasonerExtentionTests/ReasonerRegistryTest.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tests/ProofRuleTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tests/ProverChecksTests.java
    trunk/RodinCore/org.eventb.core.tests/plugin.xml
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/ProofSerializationTests.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerDesc.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IVersionedReasoner.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ReasonerDesc.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/VersionedIdCodec.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/AbstractFakeReasoner.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/FailureReasoner.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/SuccessReasoner.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/reasonerExtentionTests/ReasonerDescTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/reasonerExtentionTests/ReasonerV1.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/ReasonerV2.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7507
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7507&view=rev
Author:   nicolas_beauger
Date:     2009-09-02 12:20:17 +0000 (Wed, 02 Sep 2009)

Log Message:
-----------
Introduced generated elements: added interface IGeneratedElement.
IEventBRoot implements IGeneratedElement (i.e can be added a 'generated' attribute).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBElement.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IGeneratedElement.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/GeneratedElementsTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7590
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7590&view=rev
Author:   carinepascal
Date:     2009-10-07 16:30:41 +0000 (Wed, 07 Oct 2009)

Log Message:
-----------
The POG does not not generate any longer THM POs for guards when the conditions have already been proved for the abstract event.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/PredicateModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/EventBPOTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineRefines.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7700
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7700&view=rev
Author:   spooky23
Date:     2009-10-22 12:33:12 +0000 (Thu, 22 Oct 2009)

Log Message:
-----------
Trace option for Recalculate Auto Status

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/.options
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBProofElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/RecalculateAutoStatus.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 7979
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=7979&view=rev
Author:   thomasmuller
Date:     2009-12-18 17:22:07 +0000 (Fri, 18 Dec 2009)

Log Message:
-----------
Fixed bug ID: 2815882 - Primed identifiers are allowed.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/IdentifierModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventWitnessModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GenericIdentTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8091
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8091&view=rev
Author:   nicolas_beauger
Date:     2010-01-21 15:19:16 +0000 (Thu, 21 Jan 2010)

Log Message:
-----------
Autocompletion: took extended events into account.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/CompletionUtil.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/EnumeratedFilter.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8286
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8286&view=rev
Author:   nicolas_beauger
Date:     2010-02-17 15:50:57 +0000 (Wed, 17 Feb 2010)

Log Message:
-----------
Event-B Core plug-in: incremented version to 1.3; updated @since reference.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/state/SymbolFactory.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8336
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8336&view=rev
Author:   nicolas_beauger
Date:     2010-02-24 14:05:52 +0000 (Wed, 24 Feb 2010)

Log Message:
-----------
Fixed Bug #2952087: Rodin 1.2 reuses erroneous Rodin 1.1 proof.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/PSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/PSUpdater.java
    trunk/RodinCore/org.eventb.core.seqprover/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverLib.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/proofBuilder/ProofBuilder.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/ProofBuilderTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8348
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8348&view=rev
Author:   nicolas_beauger
Date:     2010-02-26 17:33:38 +0000 (Fri, 26 Feb 2010)

Log Message:
-----------
Event-B Core: implemented a proof rebuild operation for feature request #2949606: Add a replay proof command in event-B explorer

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofSimplifier.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofModifier.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofRebuilder.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/proofSimplifier/ProofRebuilderTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8451
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8451&view=rev
Author:   nicolas_beauger
Date:     2010-03-15 16:35:44 +0000 (Mon, 15 Mar 2010)

Log Message:
-----------
Introduced the notion of PO nature (IPOGNature).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOSequent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POSequent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/POGProcessorModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/ContextAxiomModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionBodySimModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionFrameSimModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventStrengthenGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventVariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventWitnessModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineInvariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineNewEventInvariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineRefEventInvariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineVariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/PredicateModule.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/IPOGNature.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/POGNature.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/POGNatureFactory.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestNature.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8462
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8462&view=rev
Author:   a_gilles
Date:     2010-03-19 09:41:47 +0000 (Fri, 19 Mar 2010)

Log Message:
-----------
Added origin of predicates in proof

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCPredicateElement.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/EventBTest.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/OriginTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8552
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8552&view=rev
Author:   nicolas_beauger
Date:     2010-03-30 14:51:57 +0000 (Tue, 30 Mar 2010)

Log Message:
-----------
Auto completion: propose disappearing variables in invariants.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8570
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8570&view=rev
Author:   lvoisin
Date:     2010-03-31 16:41:18 +0000 (Wed, 31 Mar 2010)

Log Message:
-----------
Code review of AutoCompletion (small non-functional changes + more tests).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/autocompletion/AutoCompletionTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 8762
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=8762&view=rev
Author:   thomasmuller
Date:     2010-05-10 10:46:17 +0000 (Mon, 10 May 2010)

Log Message:
-----------
Refactored initialization repairing using createChild() method, no functional change. Added related test.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventActionModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEvents.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9095
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9095&view=rev
Author:   lvoisin
Date:     2010-06-08 16:53:20 +0000 (Tue, 08 Jun 2010)

Log Message:
-----------
Added method IProofComponent.getProofAttempt(poName, owner).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProofComponent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofComponent.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pm/ProofComponentTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9130
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9130&view=rev
Author:   lvoisin
Date:     2010-06-10 15:11:11 +0000 (Thu, 10 Jun 2010)

Log Message:
-----------
Fixed API compatibility problem in org.eventb.core.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProofComponent.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9431
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9431&view=rev
Author:   lvoisin
Date:     2010-07-20 16:20:19 +0000 (Tue, 20 Jul 2010)

Log Message:
-----------
Merged back branch 2.0 into trunk for plug-in org.eventb.core.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ProofStoreReader.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProofAttempt.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProofComponent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/StaticChecker.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/tool/IStateRepository.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/EventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/PSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/ProofSkeletonBuilder.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/AutoCompletion.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/autocompletion/CompletionUtil.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/AssignmentIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ElementIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventBIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/EventIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/ExpressionIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/FormulaIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/IdentTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/MachineIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/indexers/PredicateIndexer.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofAttempt.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofComponent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofState.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/POGStateRepository.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventHypothesesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/UtilityModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POLoader.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/PSUpdater.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/SCStateRepository.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/BaseModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/ContextPointerModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/IdentifierModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/LabeledFormulaModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventActionModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventWitnessFreeIdentsModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventWitnessModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineRefinesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineVariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/symbolTable/IdentifierSymbolTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/symbolTable/StackedIdentifierSymbolTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/tool/state/StateRepository.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/upgrade/UpgraderV1V2.java

Property Changed:
----------------
    trunk/RodinCore/org.eventb.core/
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/RecalculateAutoStatus.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9581
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9581&view=rev
Author:   thomasmuller
Date:     2010-08-17 09:36:29 +0000 (Tue, 17 Aug 2010)

Log Message:
-----------
Defined a mechanism to provide formula extensions through formula extension providers (see IFormulaExtensionProvider) :
 * Added org.eventb.core.formulaExtensionProvider extension point,
 * Implemented a registry for formula extension providers (see IFormulaExtensionProviderRegistry),
 * Modified FormulaFactory and EventBProject to retrieve extensions from the formula extension provider registry. 
Added tests to check that this mechanism works.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/EventBProject.java
    trunk/RodinCore/org.eventb.core.ast/src/org/eventb/core/ast/FormulaFactory.java
    trunk/RodinCore/org.eventb.core.tests/plugin.xml

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/schema/formulaExtensionProviders.exsd
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IFormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/FormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/FormulaExtensionProviderRegistryTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/Prime.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/PrimeFormulaExtensionProvider.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9610
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9610&view=rev
Author:   thomasmuller
Date:     2010-08-30 14:54:39 +0000 (Mon, 30 Aug 2010)

Log Message:
-----------
Implemented Feature Request #3055966 - Warning for INITIALIZATION. A warning is now created when the user seems to have mispelled INITIALISATION.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/GraphProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GraphProblemTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEvents.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9624
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9624&view=rev
Author:   thomasmuller
Date:     2010-09-03 14:40:27 +0000 (Fri, 03 Sep 2010)

Log Message:
-----------
Pulled-up isTrivial() from UtilityModule to POGProcessorModule. Used isTrivial() in createPO() to avoid creating trivial POs. Corrected tests accordingly.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/POGProcessorModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionBodySimModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventActionModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventStrengthenGuardModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineEventWitnessModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/FwdMachineVariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/MachineEventInvariantModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/PredicateModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/modules/UtilityModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pog/TestMachineEvents.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9696
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9696&view=rev
Author:   nicolas_beauger
Date:     2010-09-10 17:04:33 +0000 (Fri, 10 Sep 2010)

Log Message:
-----------
Formula provider extension: moved interface to sub-package, removed interface for registry, moved registry code to an internal package.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/schema/formulaExtensionProviders.exsd
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/EventBProject.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/FormulaExtensionProviderRegistryTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/PrimeFormulaExtensionProvider.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/FormulaExtensionProviderRegistry.java

Removed Paths:
-------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IFormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/FormulaExtensionProviderRegistry.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9742
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9742&view=rev
Author:   nicolas_beauger
Date:     2010-09-14 17:57:43 +0000 (Tue, 14 Sep 2010)

Log Message:
-----------
Fixed bug 3053075 : hypothesis gets deselected unexpectedly.
added a notion of unselected hypotheses, which are deselected only if not previously selected.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBProofElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRRuleAntecedent.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverFactory.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverLib.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/IInternalProverSequent.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ProverSequent.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tests/ProverSequentTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9756
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9756&view=rev
Author:   thomasmuller
Date:     2010-09-15 17:04:31 +0000 (Wed, 15 Sep 2010)

Log Message:
-----------
Modified granularity of the getFormulaFactory() method. The element passed through this method calls is now an IEventBRoot element itself (instead of IEventBProject element).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/EventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/FormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/FormulaExtensionProviderRegistryTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/PrimeFormulaExtensionProvider.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9760
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9760&view=rev
Author:   thomasmuller
Date:     2010-09-16 12:42:19 +0000 (Thu, 16 Sep 2010)

Log Message:
-----------
Added setFormulaFactory(root, ff) for each root element, so that getFormulaFactory(root) must return the previously set factory;
Modified the formula extension provider registry : only one provider can be registered now.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/EventBProject.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/FormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/PrimeFormulaExtensionProvider.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9805
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9805&view=rev
Author:   nicolas_beauger
Date:     2010-09-23 12:43:35 +0000 (Thu, 23 Sep 2010)

Log Message:
-----------
org.eventb.core plug-in: incremented major version number because of major version changes in re-exported plug-ins.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ProofStoreReader.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProofAttempt.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IUserSupport.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pog/POGProcessorModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/GraphProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/ParseProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/tool/IStateRepository.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9815
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9815&view=rev
Author:   nicolas_beauger
Date:     2010-09-24 08:49:33 +0000 (Fri, 24 Sep 2010)

Log Message:
-----------
Extension API: added methods for retrieving files whose modification require a rebuild.
Added dependency from these files to the corresponding builder-generated files.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/extension/IFormulaExtensionProvider.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/FormulaExtensionProviderRegistry.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/Util.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/ContextProofObligationGenerator.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pog/MachineProofObligationGenerator.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/AutoPOM.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/ContextStaticChecker.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/MachineStaticChecker.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/extension/PrimeFormulaExtensionProvider.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 9907
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=9907&view=rev
Author:   thomasmuller
Date:     2010-10-04 14:16:27 +0000 (Mon, 04 Oct 2010)

Log Message:
-----------
Fixed bug #2174629 - No PO generated for unrefined event.
A warning is now generated on the refinement indicating that a given event was not explicitely closed if an abstract event is not refined, and does not contain the false guard. In fact, to close a given event, it is asked to the user to explicitely add the "false" guard to event (e.g. a guard containing the literal predicate "false"). 

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/GraphProblem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/state/IAbstractEventInfo.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/state/IConcreteEventTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/AbstractEventInfo.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/ConcreteEventTable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventRefinesModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/GraphProblemTest.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEventRefines.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 10259
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=10259&view=rev
Author:   nicolas_beauger
Date:     2010-11-09 10:34:00 +0000 (Tue, 09 Nov 2010)

Log Message:
-----------
Declared tactic "Datatype Destructor WD" as auto and post tactic; also added it to the list of default auto and post tactics.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/PostTacticPreference.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POMTacticPreference.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 10261
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=10261&view=rev
Author:   lvoisin
Date:     2010-11-09 17:38:03 +0000 (Tue, 09 Nov 2010)

Log Message:
-----------
Fix bug 3106076: Missing POs in interface.

Added checks for errors when fetching proof skeletons from proof files
and isolating such faults so that they do not propagate and break POM.
Done the same work for the proving UI (i.e., in UserSupport).

In the longer term, it might be interesting to recover a partial skeleton,
ignoring only the subtree rooted to an ill-formed node.  Also, currently,
in case of error, the problem is only traced in the log but not displayed
in the GUI (as the current protocol doesn't allow to report such problems).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/PSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProofState.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/PSUpdater.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/PSUpdateTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/ProofSerializationTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 10759
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=10759&view=rev
Author:   thomasmuller
Date:     2011-02-03 15:16:23 +0000 (Thu, 03 Feb 2011)

Log Message:
-----------
Implemented FR #3137919 - Automatic "Apply membership" tactics and FR #3137897 - Add an equivalence rewriting auto tactic.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/Tactics.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TreeShape.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/AutoEqvTacTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/AutoRmiTacTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TacticTestUtils.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11028
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11028&view=rev
Author:   nicolas_beauger
Date:     2011-03-18 10:20:58 +0000 (Fri, 18 Mar 2011)

Log Message:
-----------
Reintegrated branch ProofDeps.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPRProof.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IProofStoreCollector.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IProofStoreReader.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBProofElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRProof.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRProofRule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ProofStoreCollector.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ProofStoreReader.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/PSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/PSUpdater.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IProofDependencies.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerDesc.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverFactory.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverLib.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ProofDependenciesBuilder.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/proofBuilderTests/ProofBuilderTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tests/ProofRuleTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tests/ProofTreeTests.java
    trunk/RodinCore/org.eventb.core.tests/META-INF/MANIFEST.MF
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pm/ProofAttemptTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/PSUpdateTests.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/ProofSerializationTests.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPRReasoner.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRReasoner.java

Property Changed:
----------------
    trunk/RodinCore/org.eventb.core/
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/Messages.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/messages.properties
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/RecalculateAutoStatus.java
    trunk/RodinCore/org.eventb.core.seqprover/
    trunk/RodinCore/org.eventb.core.seqprover.tests/
    trunk/RodinCore/org.eventb.core.tests/


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11264
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11264&view=rev
Author:   nicolas_beauger
Date:     2011-04-15 09:50:06 +0000 (Fri, 15 Apr 2011)

Log Message:
-----------
Implemented standard refinement participants for contexts and machine (copied code from ui).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/refinement/
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/refinement/ExtendContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/refinement/RefineMachine.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11311
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11311&view=rev
Author:   billaude
Date:     2011-04-20 09:27:27 +0000 (Wed, 20 Apr 2011)

Log Message:
-----------
Negation Normal Form is now available in post-tactics and auto-tactics.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/PostTacticPreference.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POMTacticPreference.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11598
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11598&view=rev
Author:   billaude
Date:     2011-05-11 16:30:58 +0000 (Wed, 11 May 2011)

Log Message:
-----------
Generalized Modus Ponens is now available in Post-tactics and Auto-tactics.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/PostTacticPreference.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POMTacticPreference.java
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11636
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11636&view=rev
Author:   lvoisin
Date:     2011-05-13 17:18:17 +0000 (Fri, 13 May 2011)

Log Message:
-----------
Fix bug #3301649: Marker for unrefined event invisible.

The marker is now associated with the refines clause.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/state/IAbstractEventInfo.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/AbstractEventInfo.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineEventRefinesModule.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/sc/modules/MachineRefinesModule.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/sc/TestEventRefines.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11645
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11645&view=rev
Author:   billaude
Date:     2011-05-16 09:59:57 +0000 (Mon, 16 May 2011)

Log Message:
-----------
Adding the tactic GoalDisjSTac which remove disjunction only in the goal's root (applying DisjToImpl then ImpI).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TreeShape.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/GoalDisjToImpl.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/GoalDisjSTacTests.java

Removed Paths:
-------------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11646
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11646&view=rev
Author:   nicolas_beauger
Date:     2011-05-16 13:03:53 +0000 (Mon, 16 May 2011)

Log Message:
-----------
Added API problem filters for getEventBProject()

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/sc/state/IAbstractEventInfo.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core/.settings/.api_filters


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11652
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11652&view=rev
Author:   billaude
Date:     2011-05-16 16:02:49 +0000 (Mon, 16 May 2011)

Log Message:
-----------
GoalDisjToImpl remove from org.eventb.sor.seqprover.eventbExtensions.tactics and added in the class DisjGoalTac (in the autotactics).
Change in the tests presentation (for consistency of the code).
Change of tactic's name (from GoalDisjSTac to DisjGoalTac).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/DisjGoalTacTests.java

Removed Paths:
-------------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/GoalDisjToImpl.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/GoalDisjSTacTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11685
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11685&view=rev
Author:   billaude
Date:     2011-05-18 15:43:02 +0000 (Wed, 18 May 2011)

Log Message:
-----------
NNFRewritesAutoTac is now available in Post-tactics and Auto-tactics.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/PostTacticPreference.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POMTacticPreference.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11709
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11709&view=rev
Author:   lvoisin
Date:     2011-05-22 21:00:29 +0000 (Sun, 22 May 2011)

Log Message:
-----------
Fix bug 3303436: Complicated WD hypothesis popping up

Changed test for including WD predicates when loading proofs.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pom/POLoader.java
    trunk/RodinCore/org.eventb.core.tests/src/org/eventb/core/tests/pom/POLoaderTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 11786
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=11786&view=rev
Author:   nicolas_beauger
Date:     2011-05-30 18:11:14 +0000 (Mon, 30 May 2011)

Log Message:
-----------
Implemented signature for reasoners.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRReasoner.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ProofStoreCollector.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerDesc.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/IReasonerRegistry.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ProverLib.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ReasonerDesc.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/ReasonerRegistry.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/ISignatureReasoner.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12112
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12112&view=rev
Author:   billaude
Date:     2011-06-22 07:53:18 +0000 (Wed, 22 Jun 2011)

Log Message:
-----------
New reasoner (and its auto-tactic) discharging sequent such as : f(x)?\226?\136?\136S, S?\226?\138?\134T (or S?\226?\138?\130T) ?\226?\138?\162 f(x)?\226?\136?\136T.
Plus the tests of the reasoner.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TreeShape.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/FunImgInclusionGoal.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/eventbExtentionTests/FunImgInclusionGoalTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12113
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12113&view=rev
Author:   billaude
Date:     2011-06-22 08:25:34 +0000 (Wed, 22 Jun 2011)

Log Message:
-----------
Adding the tactic FunAppInDomGoalTac which try to discharge a sequent whose goal is such as : f(x)?\226?\136?\136dom(g) by calling three tactic :
 - FunImageGoal (add an hypothesis such as f(x)?\226?\136?\136S)
 - TotalDomRewrites (replace dom(g) by a set : T)
 - FunImgInclusionGoal (discharge a sequent such as f(x)?\226?\136?\136S, S?\226?\138?\134T (or S?\226?\138?\130T) ?\226?\138?\162 f(x)?\226?\136?\136T)

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/FunAppInDomGoalTac.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/FunAppInDomGoalAutoTacTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12580
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12580&view=rev
Author:   lvoisin
Date:     2011-07-25 15:32:12 +0000 (Mon, 25 Jul 2011)

Log Message:
-----------
Code review for bug fix #3370087

No functional change.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRProofRule.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/rewriters/ContImplHypRewrites.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12772
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12772&view=rev
Author:   billaude
Date:     2011-08-19 15:45:37 +0000 (Fri, 19 Aug 2011)

Log Message:
-----------
Modifying the reasoner FunImgInclusionGoal into MembershipGoal.
Adding the corresponding tests, as well as the class used for the reasoner (MyPosition and Rules, and so RulesTests).
Adding the TreeShape corresponding to that reasoner.

Modifying the existing tactic FunAppInDomGoalTax in consequences.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/FunAppInDomGoalTac.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/FunAppInDomGoalAutoTacTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TreeShape.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/reasonerInputs/HypothesesReasoner.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/MembershipGoal.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/MyPosition.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/Rule.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/MembershipGoalTac.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/eventbExtentionTests/MembershipGoalTests.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/eventbExtentionTests/RuleTest.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/MembershipGoalTacTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12774
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12774&view=rev
Author:   billaude
Date:     2011-08-19 16:04:53 +0000 (Fri, 19 Aug 2011)

Log Message:
-----------
Adding the reasoner MapOvrGoal, as well as its tests and its associated tactic.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/MapOvrGoal.java
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/MapOvrGoalTac.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/eventbExtentionTests/MapOvrGoalTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 12781
          http://rodin-b-sharp.svn.sourceforge.net/rodin-b-sharp/?rev=12781&view=rev
Author:   billaude
Date:     2011-08-22 07:05:18 +0000 (Mon, 22 Aug 2011)

Log Message:
-----------
Committing the tactic TotalDomToCProdTac which substitutes in the goal a domain by a cartesian product.
The goal must match : x?\226?\134?\166y?\226?\136?\136dom(g).

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/plugin.properties
    trunk/RodinCore/org.eventb.core.seqprover/plugin.xml
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/core/seqprover/eventbExtensions/AutoTactics.java

Added Paths:
-----------
    trunk/RodinCore/org.eventb.core.seqprover/src/org/eventb/internal/core/seqprover/eventbExtensions/tactics/TotalDomToCProdTac.java
    trunk/RodinCore/org.eventb.core.seqprover.tests/src/org/eventb/core/seqprover/tactics/tests/TotalDomToCProdTacTests.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 15358
          http://sourceforge.net/p/rodin-b-sharp/svn/15358
Author:   lvoisin
Date:     2012-12-17 16:39:36 +0000 (Mon, 17 Dec 2012)
Log Message:
-----------
Cleanup Event-B database layer.

Remove all deprecated classes and methods in the database customization
for Event-B.

Modified Paths:
--------------
    trunk/RodinCore/org.eventb.core/plugin.properties
    trunk/RodinCore/org.eventb.core/plugin.xml
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBAttributes.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/EventBPlugin.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IAssignmentElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IExpressionElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IExtendsContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IIdentifierElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOIdentifier.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOPredicate.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOPredicateSet.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOSequent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPOSource.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPSStatus.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IRefinesEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IRefinesMachine.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCAssignmentElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCExpressionElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCIdentifierElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCRefinesEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCRefinesMachine.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCVariable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISeesContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Event.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/ExtendsContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/MachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POIdentifier.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POPredicate.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POPredicateSet.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POSequent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/POSource.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRHypAction.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PRRuleAntecedent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/PSStatus.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/RefinesEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/RefinesMachine.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCAssignmentElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCContextRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCExpressionElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCIdentifierElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCInternalContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCMachineRoot.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCPredicateElement.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCRefinesEvent.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCRefinesMachine.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCVariable.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SeesContext.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IUserSupportManager.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/UserSupportManager.java

Removed Paths:
-------------
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/IPSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ISCTheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/ITheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/CommonAttributesUtil.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/EventBUtil.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/SCTheorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/basis/Theorem.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/core/pm/IProvingMode.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/PSWrapper.java
    trunk/RodinCore/org.eventb.core/src/org/eventb/internal/core/pm/ProvingMode.java

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.