From 90d26251ef775c8c5f683c3a70c957f78bffbaf1 Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Thu, 17 Jul 2014 10:12:56 +0200 Subject: [PATCH] integration commit between camille 2 and 3, merging the multiple lines of development (git + svn), includes rodin 3 port Sadly, it was not possible to generate separate commits out of this as these did not exist in the former repositories --- build.gradle | 4 +- de.be4.eventb.structparser/.classpath | 9 +- de.be4.eventb.structparser/.project | 3 +- .../EventBParser.sablecc | 28 +- de.be4.eventb.structparser/customBuild.xml | 44 +-- .../be4/eventb/core/parser/EventBLexer.java | 6 +- .../be4/eventb/core/parser/EventBParser.java | 3 - .../eventb/core/parser/lexer/LexerAspect.aj | 24 -- org.eventb.texteditor.feature/.classpath | 5 + org.eventb.texteditor.feature/.project | 20 +- .../.settings/org.eclipse.jdt.core.prefs | 19 +- org.eventb.texteditor.feature/camille.target | 10 +- org.eventb.texteditor.feature/category.xml | 7 + org.eventb.texteditor.feature/feature.xml | 16 +- org.eventb.texteditor.feature/pom.xml | 16 + org.eventb.texteditor.parent/pom.xml | 90 +++++ org.eventb.texteditor.repository/category.xml | 15 + org.eventb.texteditor.repository/pom.xml | 18 + org.eventb.texteditor.ui/.classpath | 2 +- org.eventb.texteditor.ui/.project | 28 +- .../.settings/org.eclipse.jdt.core.prefs | 7 - org.eventb.texteditor.ui/META-INF/MANIFEST.MF | 9 +- org.eventb.texteditor.ui/pom.xml | 19 + org.eventb.texttools.test/.classpath | 7 - org.eventb.texttools.test/.project | 28 -- .../META-INF/MANIFEST.MF | 8 - org.eventb.texttools.test/build.properties | 4 - .../org/eventb/texttools/AllTestsSuite.java | 56 --- .../formulas/ExpressionResolverTest.java | 22 -- .../formulas/ResolveVisitorTest.java | 368 ------------------ .../internal/parsing/CoreModelTest.java | 22 -- .../parsing/TransformationVisitorTest.java | 246 ------------ org.eventb.texttools/.classpath | 5 +- org.eventb.texttools/.project | 28 +- .../.settings/org.eclipse.jdt.core.prefs | 12 - org.eventb.texttools/META-INF/MANIFEST.MF | 8 +- org.eventb.texttools/build.properties | 6 +- org.eventb.texttools/pom.xml | 19 + .../texttools/diff/EventBAttributesCheck.java | 7 - .../texttools/diff/EventBReferencesCheck.java | 4 +- .../parsing/TransformationVisitor.java | 9 + .../prettyprint/ContextPrintSwitch.java | 6 +- 42 files changed, 318 insertions(+), 949 deletions(-) delete mode 100644 de.be4.eventb.structparser/src/de/be4/eventb/core/parser/lexer/LexerAspect.aj create mode 100644 org.eventb.texteditor.feature/.classpath rename {org.eventb.texttools.test => org.eventb.texteditor.feature}/.settings/org.eclipse.jdt.core.prefs (71%) create mode 100644 org.eventb.texteditor.feature/category.xml create mode 100644 org.eventb.texteditor.feature/pom.xml create mode 100644 org.eventb.texteditor.parent/pom.xml create mode 100644 org.eventb.texteditor.repository/category.xml create mode 100644 org.eventb.texteditor.repository/pom.xml delete mode 100644 org.eventb.texteditor.ui/.settings/org.eclipse.jdt.core.prefs create mode 100644 org.eventb.texteditor.ui/pom.xml delete mode 100644 org.eventb.texttools.test/.classpath delete mode 100644 org.eventb.texttools.test/.project delete mode 100644 org.eventb.texttools.test/META-INF/MANIFEST.MF delete mode 100644 org.eventb.texttools.test/build.properties delete mode 100644 org.eventb.texttools.test/src/org/eventb/texttools/AllTestsSuite.java delete mode 100644 org.eventb.texttools.test/src/org/eventb/texttools/formulas/ExpressionResolverTest.java delete mode 100644 org.eventb.texttools.test/src/org/eventb/texttools/formulas/ResolveVisitorTest.java delete mode 100644 org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/CoreModelTest.java delete mode 100644 org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/TransformationVisitorTest.java delete mode 100644 org.eventb.texttools/.settings/org.eclipse.jdt.core.prefs create mode 100644 org.eventb.texttools/pom.xml diff --git a/build.gradle b/build.gradle index 6c3da43..334de54 100644 --- a/build.gradle +++ b/build.gradle @@ -1,8 +1,8 @@ targetRepositories = ["http://www.stups.uni-duesseldorf.de/ProB/buildlibs/rodin/","http://download.eclipse.org/releases/juno/","http://rodin-b-sharp.sourceforge.net/updates"] // ps Repository with Target Definition File - + groupID = "org.eventb.texteditor" -categoryDescriptions = [["org.eventb.texteditor.feature": "Camille Text Editor"],["org.eventb.texteditor.feature": "Camille Text Editor"]] // label and descriptions of the features +categoryDescriptions = [["org.eventb.texteditor.feature": "Camille Text Editor"],["org.eventb.texteditor.feature": "Camille Text Editor"]] // label and descriptions of the features apply from: 'tycho_build.gradle' diff --git a/de.be4.eventb.structparser/.classpath b/de.be4.eventb.structparser/.classpath index 03bdf12..ee74eee 100644 --- a/de.be4.eventb.structparser/.classpath +++ b/de.be4.eventb.structparser/.classpath @@ -2,14 +2,7 @@ <classpath> <classpathentry kind="src" path="src"/> <classpathentry kind="src" path="src_generated"/> - <classpathentry kind="src" path="test"/> - <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/> - <classpathentry exported="true" kind="lib" path="lib/ParserAspects.jar"> - <attributes> - <attribute name="org.eclipse.ajdt.aspectpath" value="org.eclipse.ajdt.aspectpath"/> - </attributes> - </classpathentry> - <classpathentry exported="true" kind="lib" path="lib/aspectjrt.jar"/> + <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/> <classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/3"/> <classpathentry kind="output" path="bin"/> </classpath> diff --git a/de.be4.eventb.structparser/.project b/de.be4.eventb.structparser/.project index 7e6dbbc..4424182 100644 --- a/de.be4.eventb.structparser/.project +++ b/de.be4.eventb.structparser/.project @@ -6,13 +6,12 @@ </projects> <buildSpec> <buildCommand> - <name>org.eclipse.ajdt.core.ajbuilder</name> + <name>org.eclipse.jdt.core.javabuilder</name> <arguments> </arguments> </buildCommand> </buildSpec> <natures> - <nature>org.eclipse.ajdt.ui.ajnature</nature> <nature>org.eclipse.jdt.core.javanature</nature> </natures> </projectDescription> diff --git a/de.be4.eventb.structparser/EventBParser.sablecc b/de.be4.eventb.structparser/EventBParser.sablecc index 39f590a..bfd2f09 100644 --- a/de.be4.eventb.structparser/EventBParser.sablecc +++ b/de.be4.eventb.structparser/EventBParser.sablecc @@ -251,7 +251,10 @@ parameter {-> parameter} =[name]:identifier_literal [comment]:comment* {-> New event_where {-> guard*} = where [first]:guard [rest]:event_where_tail* {-> [first.guard, rest.guard]}; event_where_tail {-> guard} = [guard]:guard {-> guard.guard}; -guard {-> guard} = [label]:P.label [predicate]:formula [comment]:comment* {-> New guard([comment], label.label, predicate)}; +guard {-> guard} = + [label]:P.label [predicate]:formula [comment]:comment* {-> New guard([comment], label.label, predicate)} | + {derived} theorem [label]:P.label [predicate]:formula [comment]:comment* {-> New guard.derived([comment], label.label, predicate)}; + event_with {-> witness*} = with [first]:witness [rest]:event_with_tail* {-> [first.witness, rest.witness]}; event_with_tail {-> witness} = [witness]:witness {-> witness.witness}; @@ -265,15 +268,18 @@ action {-> action} = [label]:P.label [action]:formula [comment]:comment* {-> New /* Structure of a context file */ + context {-> parse_unit} = T.context [name]:identifier_literal [comment]:comment* [extends]:extends_clause? - [constants]:constants_clause? - [sets]:sets_clause? + [sets]:sets_clause? + [constants]:constants_clause? [axioms]:axioms_clause? - end {-> New parse_unit.context([comment], name, [extends.identifier_literal], [sets.carrier_set], [constants.constant], [axioms.axiom])} ; - + end {-> New parse_unit.context([comment], name, [extends.identifier_literal], [sets.carrier_set], [constants.constant], [axioms.axiom])} ; + + + extends_clause {-> identifier_literal*} = T.extends [first]:identifier_literal [rest]:extends_clause_tail* {-> [first, rest.identifier_literal]} ; extends_clause_tail {-> identifier_literal} = [name]:identifier_literal {-> name}; @@ -315,10 +321,10 @@ parse_unit = [comments]:comment* [name]:identifier_literal [extends_names]:identifier_literal* - [sets]:carrier_set* - [constants]:constant* + [sets]:carrier_set* + [constants]:constant* [axioms]:axiom*; - + variable = [comments]:comment* [name]:identifier_literal; variant = [comments]:comment* [expression]:formula ; invariant = @@ -348,6 +354,10 @@ event_refinement = {extended} [name]:identifier_literal ; parameter = [comments]:comment* [name]:identifier_literal; -guard = [comments]:comment* [name]:label [predicate]:formula ; + +guard = + [comments]:comment* [name]:label [predicate]:formula | + {derived} [comments]:comment* [name]:label [predicate]:formula; + witness = [comments]:comment* [name]:label [predicate]:formula ; action = [comments]:comment* [name]:label [action]:formula ; diff --git a/de.be4.eventb.structparser/customBuild.xml b/de.be4.eventb.structparser/customBuild.xml index 21c0f41..f0b8647 100644 --- a/de.be4.eventb.structparser/customBuild.xml +++ b/de.be4.eventb.structparser/customBuild.xml @@ -13,13 +13,9 @@ <property name="dir.release" location="release"/> <property name="file.release.jar" location="${dir.release}\EventBParser.jar" /> - <property name="file.parseraspects.jar" location="lib/ParserAspects.jar" /> - <property name="file.aspectjrt.jar" location="lib/aspectjrt.jar" /> - + <taskdef name="sablecc" classname="org.sablecc.ant.taskdef.Sablecc" classpath="lib/ext/sablecc-anttask.jar" /> - <taskdef resource="org/aspectj/tools/ant/taskdefs/aspectjTaskdefs.properties" classpath="lib/ext/aspectjtools.jar" /> - <target name="init"> <mkdir dir="${dir.temp.classes}" /> <mkdir dir="${dir.temp.src}" /> @@ -45,39 +41,33 @@ </target> <target name="compile" depends="init,sablecc-parser" description=""> - <iajc - fork="true" - destdir="${dir.temp.classes}" - source="1.5" - sourceRootCopyFilter="**/*.java,**/.svn/*" - inpathDirCopyFilter="**/*.java,**/.svn/*" > - <sourceroots> - <pathelement location="src_generated"/> - <pathelement location="src"/> - </sourceroots> - <inpath> - <pathelement location="${file.parseraspects.jar}" /> - </inpath> - <classpath> - <pathelement location="${file.aspectjrt.jar}" /> - </classpath> - </iajc> - </target> + <copy todir="${dir.temp.src}"> + <fileset dir="src"/> + <fileset dir="src_generated"/> + </copy> + + <javac srcdir="${dir.temp.src}" destdir="${dir.temp.classes}" includeAntRuntime="false" target="1.5" source="1.5"/> + + <copy file="src_generated/de/be4/eventb/core/parser/lexer/lexer.dat" todir="${dir.temp.classes}/de/be4/eventb/core/parser/lexer" /> + <copy file="src_generated/de/be4/eventb/core/parser/parser/parser.dat" todir="${dir.temp.classes}/de/be4/eventb/core/parser/parser" /> + </target> <target name="jar" depends="init,compile" description=""> + <tstamp> + <format property="TODAY" pattern="yyyy-MM-dd HH:mm:ss" /> + </tstamp> + <jar basedir="${dir.temp.classes}" destfile="${file.release.jar}" > <manifest> - <attribute name="Built-By" value="${user.name} "/> - <attribute name="Built-On" value="${TODAY} "/> + <attribute name="Built-By" value="${user.name}"/> + <attribute name="Built-On" value="${TODAY}"/> <attribute name="Main-Class" value="de.be4.eventb.core.parser.EventBParser"/> </manifest> </jar> - <delete dir="${dir.temp.classes}" /> </target> <target name="dist" depends="jar" > - <copy file="${file.aspectjrt.jar}" todir="${dir.release}" /> <delete dir="${dir.temp}" /> </target> diff --git a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBLexer.java b/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBLexer.java index a6ee876..7e70966 100644 --- a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBLexer.java +++ b/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBLexer.java @@ -36,8 +36,8 @@ public class EventBLexer extends Lexer { "The variant is only allowed after invariants and before events", "The events clause is only allowed at the end", "'context' is only allowed at the beginning of a file", - "Constant declarations are only allowed before the set declarations", - "Set declarations are only allowed allowed after constants and before axioms", + "Set declarations are only allowed before the constants declarations", + "Constants declarations are only allowed after sets and before axioms", "The axioms clause is only allowed at the end" }; private static List<String> clausesOrder = new LinkedList<String>(); private int lastClauseIndex; @@ -58,8 +58,8 @@ public class EventBLexer extends Lexer { clausesOrder.add("TVariant"); clausesOrder.add("TEvents"); clausesOrder.add("TContext"); - clausesOrder.add("TConstants"); clausesOrder.add("TSets"); + clausesOrder.add("TConstants"); clausesOrder.add("TAxioms"); eventClausesOrder.add("TAny"); eventClausesOrder.add("TWhere"); diff --git a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBParser.java b/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBParser.java index 6af7bc8..d9b7487 100644 --- a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBParser.java +++ b/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/EventBParser.java @@ -10,8 +10,6 @@ import java.io.StringReader; import java.util.List; import java.util.Map; -import com.sun.org.apache.xerces.internal.impl.xpath.regex.ParseException; - import de.be4.eventb.core.parser.analysis.ASTDisplay; import de.be4.eventb.core.parser.analysis.ASTPrinter; import de.be4.eventb.core.parser.lexer.LexerException; @@ -166,7 +164,6 @@ public class EventBParser { * </ul> * </p> */ - @SuppressWarnings("unchecked") public Start parse(final String input, final boolean debugOutput) throws BException { final Reader reader = new StringReader(input); diff --git a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/lexer/LexerAspect.aj b/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/lexer/LexerAspect.aj deleted file mode 100644 index 267850d..0000000 --- a/de.be4.eventb.structparser/src/de/be4/eventb/core/parser/lexer/LexerAspect.aj +++ /dev/null @@ -1,24 +0,0 @@ -package de.be4.eventb.core.parser.lexer; - -import de.be4.eventb.core.parser.EventBLexerException; -import de.be4.eventb.core.parser.node.Token; -import de.be4.eventb.core.parser.node.TComment; - -public privileged aspect LexerAspect pertarget(peek(Lexer)) { - - pointcut peek(Lexer lexer) : execution(Token peek()) && target(lexer); - - after(Lexer lexer) throwing(LexerException e) throws LexerException : peek(lexer) { - // if exception is already converted just throw it - if (e instanceof EventBLexerException){ - throw e; - } - - // otherwise convert exception to contain last position and text - final int line = lexer.line; - final int pos = lexer.pos; - final StringBuffer text = lexer.text; - - throw new EventBLexerException(lexer.token, e.getMessage(), text.toString(), line, pos); - } -} diff --git a/org.eventb.texteditor.feature/.classpath b/org.eventb.texteditor.feature/.classpath new file mode 100644 index 0000000..fb884b4 --- /dev/null +++ b/org.eventb.texteditor.feature/.classpath @@ -0,0 +1,5 @@ +<?xml version="1.0" encoding="UTF-8"?> +<classpath> + <classpathentry kind="output" path="bin"/> + <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER" exported="true"/> +</classpath> diff --git a/org.eventb.texteditor.feature/.project b/org.eventb.texteditor.feature/.project index 397bf70..908418b 100644 --- a/org.eventb.texteditor.feature/.project +++ b/org.eventb.texteditor.feature/.project @@ -1,17 +1,21 @@ <?xml version="1.0" encoding="UTF-8"?> <projectDescription> <name>org.eventb.texteditor.feature</name> - <comment></comment> - <projects> - </projects> + <comment/> + <projects/> + <natures> + <nature>org.eclipse.pde.FeatureNature</nature> + <nature>org.eclipse.jdt.core.javanature</nature> + </natures> <buildSpec> <buildCommand> <name>org.eclipse.pde.FeatureBuilder</name> - <arguments> - </arguments> + <arguments/> + </buildCommand> + <buildCommand> + <name>org.eclipse.jdt.core.javabuilder</name> + <arguments/> </buildCommand> </buildSpec> - <natures> - <nature>org.eclipse.pde.FeatureNature</nature> - </natures> + <linkedResources/> </projectDescription> diff --git a/org.eventb.texttools.test/.settings/org.eclipse.jdt.core.prefs b/org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs similarity index 71% rename from org.eventb.texttools.test/.settings/org.eclipse.jdt.core.prefs rename to org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs index cc5ef69..c5bb454 100644 --- a/org.eventb.texttools.test/.settings/org.eclipse.jdt.core.prefs +++ b/org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs @@ -1,12 +1,13 @@ -#Mon May 11 11:59:07 CEST 2009 -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5 -org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve -org.eclipse.jdt.core.compiler.compliance=1.5 -org.eclipse.jdt.core.compiler.debug.lineNumber=generate +# +#Wed Jun 25 10:22:53 CEST 2014 org.eclipse.jdt.core.compiler.debug.localVariable=generate +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve org.eclipse.jdt.core.compiler.debug.sourceFile=generate -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.source=1.5 +org.eclipse.jdt.core.compiler.debug.lineNumber=generate +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.source=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error diff --git a/org.eventb.texteditor.feature/camille.target b/org.eventb.texteditor.feature/camille.target index b510d11..5c04d5c 100644 --- a/org.eventb.texteditor.feature/camille.target +++ b/org.eventb.texteditor.feature/camille.target @@ -1,7 +1,7 @@ <?xml version="1.0" encoding="UTF-8" standalone="no"?> -<?pde version="3.8"?><target name="prob_target" sequenceNumber="34"> +<?pde version="3.8"?><target name="prob_target" sequenceNumber="36"> <locations> -<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit"> +<location includeAllPlatforms="true" includeConfigurePhase="false" includeMode="slicer" includeSource="true" type="InstallableUnit"> <unit id="org.rodinp.platform.sources.feature.group" version="3.0.0.201403141545-e3d282b"/> <unit id="org.eventb.ide.feature.group" version="3.0.0.201403141545-e3d282b"/> <unit id="org.rodinp.platform.tests.feature.group" version="3.0.0.201403141545-e3d282b"/> @@ -11,15 +11,15 @@ <unit id="org.eclipse.ui.workbench" version="0.0.0"/> <repository location="http://www.stups.uni-duesseldorf.de/ProB/buildlibs/rodin/"/> </location> -<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit"> +<location includeAllPlatforms="true" includeConfigurePhase="false" includeMode="slicer" includeSource="true" type="InstallableUnit"> <unit id="org.eclipse.gef.feature.group" version="3.9.1.201308190730"/> <repository location="http://download.eclipse.org/tools/gef/updates/releases"/> </location> -<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit"> +<location includeAllPlatforms="true" includeConfigurePhase="false" includeMode="slicer" includeSource="true" type="InstallableUnit"> <unit id="org.eventb.emf.feature.feature.group" version="4.1.0"/> <repository location="http://rodin-b-sharp.sourceforge.net/updates/"/> </location> -<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit"> +<location includeAllPlatforms="true" includeConfigurePhase="false" includeMode="slicer" includeSource="true" type="InstallableUnit"> <unit id="org.eclipse.emf.sdk.feature.group" version="2.8.3.v20130125-0826"/> <unit id="org.eclipse.emf.compare.sdk.feature.group" version="1.3.3.v20130213-0806"/> <repository location="http://download.eclipse.org/releases/juno"/> diff --git a/org.eventb.texteditor.feature/category.xml b/org.eventb.texteditor.feature/category.xml new file mode 100644 index 0000000..e6e1253 --- /dev/null +++ b/org.eventb.texteditor.feature/category.xml @@ -0,0 +1,7 @@ +<?xml version="1.0" encoding="UTF-8"?> +<site> + <feature url="features/org.eventb.texteditor.feature_2.2.0.jar" id="org.eventb.texteditor.feature" version="2.2.0"> + <category name="camille"/> + </feature> + <category-def name="camille" label="camille"/> +</site> diff --git a/org.eventb.texteditor.feature/feature.xml b/org.eventb.texteditor.feature/feature.xml index 3f45abb..1f55a9a 100644 --- a/org.eventb.texteditor.feature/feature.xml +++ b/org.eventb.texteditor.feature/feature.xml @@ -2,7 +2,7 @@ <feature id="org.eventb.texteditor.feature" label="Camille TextEditor" - version="3.0.0.qualifier" + version="3.0.1.qualifier" provider-name="Heinrich-Heine University Dusseldorf" plugin="org.eventb.texteditor.ui"> @@ -10,9 +10,11 @@ A text editor for the Rodin platform to edit Event-B models ----------------------------------------------------------- Release History: -3.0.0 - Adapted Camille to Rodin 3.x +3.0.1 - Added patches from 2.2.0 to the Rodin Release +3.0.0 - Rodin 3.0 Release +2.2.0 - Theorem in guards. Order of sets and constants changed to be consistent with the Rodin editor. 2.1.4 - Be more generous regarding Rodin compatibility -2.1.3 - Bigfix release for Bug #3305107 (NPE after renaming a +2.1.3 - Bugfix release for Bug #3305107 (NPE after renaming a machine) 2.1.0.beta - Rodin 2.1.1 release compatible with EventB-EMF Framework 3.3.0 @@ -32,7 +34,7 @@ EventB-EMF-plugin v3.1.0 </description> <copyright> - Copyright (c) 2009 Heinrich-Heine University Dusseldorf. + Copyright (c) 2009-2012 Heinrich-Heine University Dusseldorf. All rights reserved. </copyright> @@ -176,20 +178,20 @@ Inc. in the United States, other countries, or both. <import plugin="org.eclipse.emf.compare.match" version="1.2.2" match="compatible"/> <import plugin="org.eclipse.core.resources" version="3.8.1" match="compatible"/> <import plugin="org.eventb.emf.core" version="3.0.0" match="greaterOrEqual"/> - </requires> + </requires> <plugin id="org.eventb.texteditor.ui" download-size="0" install-size="0" - version="0.0.0" + version="3.0.1.qualifier" unpack="false"/> <plugin id="org.eventb.texttools" download-size="0" install-size="0" - version="0.0.0" + version="3.0.1.qualifier" unpack="false"/> </feature> diff --git a/org.eventb.texteditor.feature/pom.xml b/org.eventb.texteditor.feature/pom.xml new file mode 100644 index 0000000..db190cb --- /dev/null +++ b/org.eventb.texteditor.feature/pom.xml @@ -0,0 +1,16 @@ + +<?xml version="1.0" encoding="UTF-8"?> + <project + xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"> + <modelVersion>4.0.0</modelVersion> + <parent> + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.parent</artifactId> + <version>1.0.0.qualifier</version> + <relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath> + </parent> + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.feature</artifactId> + <version>3.0.1.qualifier</version> + <packaging>eclipse-feature</packaging> + </project> diff --git a/org.eventb.texteditor.parent/pom.xml b/org.eventb.texteditor.parent/pom.xml new file mode 100644 index 0000000..7959d13 --- /dev/null +++ b/org.eventb.texteditor.parent/pom.xml @@ -0,0 +1,90 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd"> + <modelVersion>4.0.0</modelVersion> + + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.parent</artifactId> + <version>1.0.0.qualifier</version> + + <packaging>pom</packaging> + + <!-- this is the parent POM from which all modules inherit common settings --> + <properties> + <tycho-version>0.14.1</tycho-version> + </properties> + + <repositories> + <repository> + <id>stups.cobra</id> + <url>http://cobra.cs.uni-duesseldorf.de/artifactory/repo/</url> + </repository> + + <!-- configure p2 repository to resolve against --> + + + + + <repository> + <id>targetRepository0</id> + <layout>p2</layout> + <url>http://www.stups.uni-duesseldorf.de/ProB/buildlibs/rodin/</url> + </repository> + + + + <repository> + <id>targetRepository1</id> + <layout>p2</layout> + <url>http://download.eclipse.org/releases/juno/</url> + </repository> + + + + <repository> + <id>targetRepository2</id> + <layout>p2</layout> + <url>http://rodin-b-sharp.sourceforge.net/updates</url> + </repository> + + + </repositories> + + <build> + <plugins> + <plugin> + <!-- enable tycho build extension --> + <groupId>org.eclipse.tycho</groupId> + <artifactId>tycho-maven-plugin</artifactId> + <version>0.14.1</version> + <extensions>true</extensions> + </plugin> + <plugin> + <groupId>org.eclipse.tycho</groupId> + <artifactId>tycho-compiler-plugin</artifactId> + <version>0.14.1</version> + <configuration> + <encoding>UTF-8</encoding> + <source>1.6</source> + <target>1.6</target> + <extraClasspathElements> + <extraClasspathElement> + <groupId>javafx</groupId> + <artifactId>javafx.mvn</artifactId> + <version>2.2.0-SNAPSHOT</version> + </extraClasspathElement> + </extraClasspathElements> + </configuration> + </plugin> + </plugins> + </build> + + <!-- the modules that should be built together --> + <modules> + <module>../org.eventb.texteditor.feature</module> + <module>../org.eventb.texteditor.ui</module> + <module>../org.eventb.texttools</module> + <module>../org.eventb.texteditor.repository</module> + + </modules> +</project> + \ No newline at end of file diff --git a/org.eventb.texteditor.repository/category.xml b/org.eventb.texteditor.repository/category.xml new file mode 100644 index 0000000..1195974 --- /dev/null +++ b/org.eventb.texteditor.repository/category.xml @@ -0,0 +1,15 @@ +<?xml version="1.0" encoding="UTF-8"?> +<site> + + + <feature url="features/org.eventb.texteditor.feature_3.0.1.qualifier.jar" id="org.eventb.texteditor.feature" version="3.0.1.qualifier"> + <category name="org.eventb.texteditor.feature.category"/> + </feature> + +<category-def name="org.eventb.texteditor.feature.category" label="Camille Text Editor"> + <description> +Camille Text Editor + </description> + </category-def> + +</site> diff --git a/org.eventb.texteditor.repository/pom.xml b/org.eventb.texteditor.repository/pom.xml new file mode 100644 index 0000000..fca084d --- /dev/null +++ b/org.eventb.texteditor.repository/pom.xml @@ -0,0 +1,18 @@ + +<?xml version="1.0" encoding="UTF-8"?> + <project + xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"> + <modelVersion>4.0.0</modelVersion> + <parent> + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.parent</artifactId> + <version>1.0.0.qualifier</version> + <relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath> + </parent> + + + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.repository</artifactId> + <version>1.0.0.qualifier</version> + <packaging>eclipse-repository</packaging> + </project> diff --git a/org.eventb.texteditor.ui/.classpath b/org.eventb.texteditor.ui/.classpath index cdf77e5..ad4b38c 100644 --- a/org.eventb.texteditor.ui/.classpath +++ b/org.eventb.texteditor.ui/.classpath @@ -1,8 +1,8 @@ <?xml version="1.0" encoding="UTF-8"?> <classpath> - <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/> <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> <classpathentry kind="src" path="src"/> + <classpathentry exported="true" kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/> <classpathentry kind="lib" path="lib/commons-lang-2.4.jar"/> <classpathentry kind="output" path="bin"/> </classpath> diff --git a/org.eventb.texteditor.ui/.project b/org.eventb.texteditor.ui/.project index f4c75c1..2a06124 100644 --- a/org.eventb.texteditor.ui/.project +++ b/org.eventb.texteditor.ui/.project @@ -1,34 +1,30 @@ <?xml version="1.0" encoding="UTF-8"?> <projectDescription> <name>org.eventb.texteditor.ui</name> - <comment></comment> - <projects> - </projects> + <comment/> + <projects/> + <natures> + <nature>org.eclipse.pde.PluginNature</nature> + <nature>org.eclipse.jdt.core.javanature</nature> + <nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature> + </natures> <buildSpec> <buildCommand> <name>org.eclipse.jdt.core.javabuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.ManifestBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.SchemaBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.api.tools.apiAnalysisBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> </buildSpec> - <natures> - <nature>org.eclipse.pde.PluginNature</nature> - <nature>org.eclipse.jdt.core.javanature</nature> - <nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature> - </natures> + <linkedResources/> </projectDescription> diff --git a/org.eventb.texteditor.ui/.settings/org.eclipse.jdt.core.prefs b/org.eventb.texteditor.ui/.settings/org.eclipse.jdt.core.prefs deleted file mode 100644 index bb19300..0000000 --- a/org.eventb.texteditor.ui/.settings/org.eclipse.jdt.core.prefs +++ /dev/null @@ -1,7 +0,0 @@ -#Thu Mar 26 12:38:05 CET 2009 -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5 -org.eclipse.jdt.core.compiler.compliance=1.5 -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error -org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.source=1.5 diff --git a/org.eventb.texteditor.ui/META-INF/MANIFEST.MF b/org.eventb.texteditor.ui/META-INF/MANIFEST.MF index 7502143..6470068 100644 --- a/org.eventb.texteditor.ui/META-INF/MANIFEST.MF +++ b/org.eventb.texteditor.ui/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: Camille Texteditor Bundle-SymbolicName: org.eventb.texteditor.ui;singleton:=true -Bundle-Version: 3.0.0.qualifier +Bundle-Version: 3.0.1.qualifier Bundle-Localization: plugin Bundle-Activator: org.eventb.texteditor.ui.TextEditorPlugin$Implementation Require-Bundle: org.eventb.texttools;bundle-version="[2.0.0,3.1.0)";visibility:=reexport, @@ -14,7 +14,8 @@ Require-Bundle: org.eventb.texttools;bundle-version="[2.0.0,3.1.0)";visibility:= org.eventb.core.ast;bundle-version="[3.0.0,4.0.0)", org.eclipse.ui.editors;bundle-version="[3.8.0,4.0.0)", org.eclipse.ui.ide;bundle-version="[3.8.2,4.0.0)", - org.rodinp.keyboard.ui;bundle-version="[2.0.0,3.0.0)" + org.rodinp.keyboard.ui;bundle-version="[2.0.0,3.0.0)", + org.eclipse.ui.workbench.texteditor Bundle-ActivationPolicy: lazy Bundle-RequiredExecutionEnvironment: J2SE-1.5 Bundle-ClassPath: lib/commons-lang-2.4.jar, @@ -22,6 +23,4 @@ Bundle-ClassPath: lib/commons-lang-2.4.jar, Bundle-Vendor: Heinrich-Heine University Dusseldorf Export-Package: org.eventb.texteditor.ui, org.eventb.texteditor.ui.editor -Import-Package: org.eclipse.emf.edit.ui.util, - org.eclipse.ui.texteditor.link, - org.eclipse.ui.texteditor.templates +Import-Package: org.eclipse.ui.texteditor.link diff --git a/org.eventb.texteditor.ui/pom.xml b/org.eventb.texteditor.ui/pom.xml new file mode 100644 index 0000000..6e28122 --- /dev/null +++ b/org.eventb.texteditor.ui/pom.xml @@ -0,0 +1,19 @@ +<?xml version="1.0" encoding="UTF-8"?> + <project + xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"> + <modelVersion>4.0.0</modelVersion> + + <parent> + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.parent</artifactId> + <version>1.0.0.qualifier</version> + <relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath> + </parent> + + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.ui</artifactId> + <version>3.0.1.qualifier</version> + <packaging>eclipse-plugin</packaging> + + </project> + \ No newline at end of file diff --git a/org.eventb.texttools.test/.classpath b/org.eventb.texttools.test/.classpath deleted file mode 100644 index 5e4c1fe..0000000 --- a/org.eventb.texttools.test/.classpath +++ /dev/null @@ -1,7 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<classpath> - <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> - <classpathentry kind="src" path="src"/> - <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/> - <classpathentry kind="output" path="bin"/> -</classpath> diff --git a/org.eventb.texttools.test/.project b/org.eventb.texttools.test/.project deleted file mode 100644 index 36c1ac7..0000000 --- a/org.eventb.texttools.test/.project +++ /dev/null @@ -1,28 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<projectDescription> - <name>org.eventb.texttools.test</name> - <comment></comment> - <projects> - </projects> - <buildSpec> - <buildCommand> - <name>org.eclipse.jdt.core.javabuilder</name> - <arguments> - </arguments> - </buildCommand> - <buildCommand> - <name>org.eclipse.pde.ManifestBuilder</name> - <arguments> - </arguments> - </buildCommand> - <buildCommand> - <name>org.eclipse.pde.SchemaBuilder</name> - <arguments> - </arguments> - </buildCommand> - </buildSpec> - <natures> - <nature>org.eclipse.pde.PluginNature</nature> - <nature>org.eclipse.jdt.core.javanature</nature> - </natures> -</projectDescription> diff --git a/org.eventb.texttools.test/META-INF/MANIFEST.MF b/org.eventb.texttools.test/META-INF/MANIFEST.MF deleted file mode 100644 index 8cbaba2..0000000 --- a/org.eventb.texttools.test/META-INF/MANIFEST.MF +++ /dev/null @@ -1,8 +0,0 @@ -Manifest-Version: 1.0 -Bundle-ManifestVersion: 2 -Bundle-Name: Test Fragment -Bundle-SymbolicName: org.eventb.texttools.test -Bundle-Version: 1.0.0 -Fragment-Host: org.eventb.texttools;bundle-version="0.0.1" -Bundle-RequiredExecutionEnvironment: J2SE-1.5 -Require-Bundle: org.junit diff --git a/org.eventb.texttools.test/build.properties b/org.eventb.texttools.test/build.properties deleted file mode 100644 index 34d2e4d..0000000 --- a/org.eventb.texttools.test/build.properties +++ /dev/null @@ -1,4 +0,0 @@ -source.. = src/ -output.. = bin/ -bin.includes = META-INF/,\ - . diff --git a/org.eventb.texttools.test/src/org/eventb/texttools/AllTestsSuite.java b/org.eventb.texttools.test/src/org/eventb/texttools/AllTestsSuite.java deleted file mode 100644 index 00614be..0000000 --- a/org.eventb.texttools.test/src/org/eventb/texttools/AllTestsSuite.java +++ /dev/null @@ -1,56 +0,0 @@ -package org.eventb.texttools; - -import java.util.Enumeration; - -import junit.framework.TestSuite; -import junit.runner.ClassPathTestCollector; -import junit.runner.TestCollector; - -/** - * All tests on the classpath. - */ -public class AllTestsSuite extends TestSuite { - - /** - * Returns a TestSuite containing all tests on the classpath. - * - * @return a TestSuite containing all tests on the classpath. - * @throws ClassNotFoundException - */ - @SuppressWarnings("unchecked") - public static TestSuite suite() throws ClassNotFoundException { - final TestSuite suite = new TestSuite(); - final Enumeration enumer = collectTestClasses(); - while (enumer.hasMoreElements()) { - final Class klass = Class.forName((String) enumer.nextElement()); - if (klass != null) { - suite.addTestSuite(klass); - } - } - - return suite; - } - - /** - * Returns qualified class names of classes on the classpath, whos name ends - * with "Test". - * - * @return qualified class names of classes on the classpath, whos name ends - * with "Test". - */ - @SuppressWarnings("unchecked") - private static Enumeration collectTestClasses() { - final TestCollector collector = new ClassPathTestCollector() { - @Override - public boolean isTestClass(final String classFileName) { - if (classFileName.endsWith("Test.class")) { - return true; - } else { - return false; - } - } - }; - - return collector.collectTests(); - } -} diff --git a/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ExpressionResolverTest.java b/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ExpressionResolverTest.java deleted file mode 100644 index a0f5109..0000000 --- a/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ExpressionResolverTest.java +++ /dev/null @@ -1,22 +0,0 @@ -package org.eventb.texttools.formulas; - -import junit.framework.TestCase; - -import org.eventb.emf.core.machine.MachineFactory; -import org.eventb.emf.core.machine.Variant; - -public class ExpressionResolverTest extends TestCase { - - public void testParseError() { - final String input = "x y"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - try { - FormulaResolver.resolve(emfExpr); - fail("Expected Exception was not thrown"); - } catch (final FormulaParseException e) { - assertEquals(emfExpr, e.getEmfObject()); - assertEquals(1, e.getAstProblems().size()); - } - } -} diff --git a/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ResolveVisitorTest.java b/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ResolveVisitorTest.java deleted file mode 100644 index c6999d5..0000000 --- a/org.eventb.texttools.test/src/org/eventb/texttools/formulas/ResolveVisitorTest.java +++ /dev/null @@ -1,368 +0,0 @@ -package org.eventb.texttools.formulas; - -import junit.framework.TestCase; - -import org.eclipse.emf.common.util.EList; -import org.eclipse.emf.common.util.TreeIterator; -import org.eclipse.emf.ecore.EAnnotation; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.util.EcoreUtil; -import org.eventb.core.ast.Formula; -import org.eventb.emf.core.AbstractExtension; -import org.eventb.emf.core.machine.Action; -import org.eventb.emf.core.machine.Invariant; -import org.eventb.emf.core.machine.MachineFactory; -import org.eventb.emf.core.machine.Variant; -import org.eventb.emf.formulas.AddExpression; -import org.eventb.emf.formulas.AndPredicate; -import org.eventb.emf.formulas.BExpressionResolved; -import org.eventb.emf.formulas.BFormula; -import org.eventb.emf.formulas.BecomesEqualToAssignment; -import org.eventb.emf.formulas.BecomesMemberOfAssignment; -import org.eventb.emf.formulas.BecomesSuchThatAssignment; -import org.eventb.emf.formulas.BoundIdentifierExpression; -import org.eventb.emf.formulas.EqualPredicate; -import org.eventb.emf.formulas.FALSITY; -import org.eventb.emf.formulas.ForallPredicate; -import org.eventb.emf.formulas.IdentifierExpression; -import org.eventb.emf.formulas.IdentityGenExpression; -import org.eventb.emf.formulas.IntegerLiteralExpression; -import org.eventb.emf.formulas.LessPredicate; -import org.eventb.emf.formulas.PartitionPredicate; -import org.eventb.emf.formulas.PredExpression; -import org.eventb.emf.formulas.Prj1GenExpression; -import org.eventb.emf.formulas.QuantifiedUnionExpression1; -import org.eventb.emf.formulas.SetExpression; -import org.eventb.emf.formulas.TRUE; -import org.eventb.emf.formulas.TRUTH; -import org.eventb.texttools.TextPositionUtil; -import org.eventb.texttools.model.texttools.TextRange; -import org.eventb.texttools.model.texttools.TexttoolsFactory; - -public class ResolveVisitorTest extends TestCase { - - /** - * Tests free_identifier, integer_literal, add_expression - * - * @throws FormulaParseException - */ - public void testAdd() throws FormulaParseException { - final String input = "x+5+y"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof AddExpression); - final AddExpression addExpr = (AddExpression) extension; - assertEquals(3, addExpr.getChildren().size()); - assertTrue(addExpr.getChildren().get(0) instanceof IdentifierExpression); - assertTrue(addExpr.getChildren().get(1) instanceof IntegerLiteralExpression); - } - - /** - * Tests free_identifier, EQUAL, TRUE - * - * @throws FormulaParseException - */ - public void testEqual() throws FormulaParseException { - final String input = "x=TRUE"; - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof EqualPredicate); - final EqualPredicate addExpr = (EqualPredicate) extension; - assertTrue(addExpr.getLeft() instanceof IdentifierExpression); - assertEquals("x", ((IdentifierExpression) addExpr.getLeft()).getName()); - assertTrue(addExpr.getRight() instanceof TRUE); - } - - /** - * Tests TRUTH, FALSITY and AND - * - * @throws FormulaParseException - */ - public void testAnd() throws FormulaParseException { - final String input = "\u22a4 \u2227 \u22a4 \u2227 \u22a5"; - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof AndPredicate); - final AndPredicate andPred = (AndPredicate) extension; - assertEquals(3, andPred.getChildren().size()); - assertTrue(andPred.getChildren().get(0) instanceof TRUTH); - assertTrue(andPred.getChildren().get(1) instanceof TRUTH); - assertTrue(andPred.getChildren().get(2) instanceof FALSITY); - } - - /** - * Tests KPRED - * - * @throws FormulaParseException - */ - public void testPred() throws FormulaParseException { - final String input = "pred"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof PredExpression); - } - - /** - * Tests {@link Formula#KPRJ1_GEN} - * - * @throws FormulaParseException - */ - public void testPrj1Gen() throws FormulaParseException { - final String input = "prj1"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof Prj1GenExpression); - } - - /** - * Tests Tests {@link Formula#KID_GEN} - * - * @throws FormulaParseException - */ - public void testIdentityGen() throws FormulaParseException { - final String input = "id"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof IdentityGenExpression); - } - - /** - * Tests forall predicate with 2 local variables and an equal as predicate - * - * @throws FormulaParseException - */ - public void testForall() throws FormulaParseException { - final String input = "\u2200 x,y \u00b7 x=y"; - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof ForallPredicate); - final ForallPredicate predicate = (ForallPredicate) extension; - final EList<BoundIdentifierExpression> identifiers = predicate - .getIdentifiers(); - assertEquals("x", identifiers.get(0).getName()); - assertEquals("y", identifiers.get(1).getName()); - - assertTrue(predicate.getPredicate() instanceof EqualPredicate); - final EqualPredicate equalPred = (EqualPredicate) predicate - .getPredicate(); - assertTrue(equalPred.getLeft() instanceof BoundIdentifierExpression); - assertTrue(equalPred.getRight() instanceof BoundIdentifierExpression); - } - - public void testQuantifiedUnion() throws FormulaParseException { - final String input = "\u22c3 x,y \u00b7 \u22a5 \u2223 x"; - final Variant emfExpr = MachineFactory.eINSTANCE.createVariant(); - emfExpr.setExpression(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof QuantifiedUnionExpression1); - final QuantifiedUnionExpression1 expression = (QuantifiedUnionExpression1) extension; - - assertEquals(2, expression.getIdentifiers().size()); - assertTrue(expression.getPredicate() instanceof FALSITY); - assertTrue(expression.getExpression() instanceof IdentifierExpression); - } - - public void testPartitionExpression() throws FormulaParseException { - final String input = "partition(S, {a}, {b})"; - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof PartitionPredicate); - final PartitionPredicate predicate = (PartitionPredicate) extension; - - final EList<BFormula> children = predicate.getChildren(); - assertEquals(3, children.size()); - assertTrue(children.get(0) instanceof IdentifierExpression); - assertTrue(children.get(1) instanceof SetExpression); - assertTrue(children.get(2) instanceof SetExpression); - } - - public void testBecomesEqual() throws FormulaParseException { - final String input = "x ≔ x + 1"; - final Action emfExpr = MachineFactory.eINSTANCE.createAction(); - emfExpr.setAction(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof BecomesEqualToAssignment); - final BecomesEqualToAssignment assignment = (BecomesEqualToAssignment) extension; - - assertEquals(1, assignment.getIdentifiers().size()); - final EList<IdentifierExpression> identifiers = assignment - .getIdentifiers(); - assertEquals("x", identifiers.get(0).getName()); - - assertEquals(1, assignment.getExpressions().size()); - final EList<BExpressionResolved> expressions = assignment - .getExpressions(); - assertTrue(expressions.get(0) instanceof AddExpression); - } - - public void testSuchThat() throws FormulaParseException { - final String input = "x :\u2223 x < x'"; - final Action emfExpr = MachineFactory.eINSTANCE.createAction(); - emfExpr.setAction(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof BecomesSuchThatAssignment); - final BecomesSuchThatAssignment assignment = (BecomesSuchThatAssignment) extension; - - assertEquals(1, assignment.getIdentifiers().size()); - final EList<IdentifierExpression> identifiers = assignment - .getIdentifiers(); - assertEquals("x", identifiers.get(0).getName()); - - assertTrue(assignment.getPredicate() instanceof LessPredicate); - final LessPredicate lessPred = (LessPredicate) assignment - .getPredicate(); - - assertEquals("x", ((IdentifierExpression) lessPred.getLeft()).getName()); - assertEquals("x'", ((BoundIdentifierExpression) lessPred.getRight()) - .getName()); - } - - public void testElementOf() throws FormulaParseException { - final String input = "x :\u2208 S"; - final Action emfExpr = MachineFactory.eINSTANCE.createAction(); - emfExpr.setAction(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - assertTrue(extension instanceof BecomesMemberOfAssignment); - final BecomesMemberOfAssignment assignment = (BecomesMemberOfAssignment) extension; - - assertEquals(1, assignment.getIdentifiers().size()); - final EList<IdentifierExpression> identifiers = assignment - .getIdentifiers(); - assertEquals("x", identifiers.get(0).getName()); - - assertTrue(assignment.getExpression() instanceof IdentifierExpression); - final IdentifierExpression identExpr = (IdentifierExpression) assignment - .getExpression(); - assertEquals("S", identExpr.getName()); - } - - public void testSourceAnnotations() throws FormulaParseException { - final String input = "\u2200 x,y \u00b7 x=z+5+y"; - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - final TreeIterator<Object> iterator = EcoreUtil.getAllContents( - extension, false); - while (iterator.hasNext()) { - final Object next = iterator.next(); - if (next instanceof BFormula) { - final BFormula formula = (BFormula) next; - final EAnnotation annotation = formula - .getEAnnotation(TextPositionUtil.ANNOTATION_TEXTRANGE); - assertNotNull(annotation); - } else if (next instanceof EAnnotation) { - final EAnnotation annotation = (EAnnotation) next; - assertNotNull(annotation.getEModelElement()); - assertNotNull(TextPositionUtil.getTextRange(annotation - .getEModelElement())); - } else if (next instanceof TextRange) { - final TextRange range = (TextRange) next; - assertTrue(range.getOffset() + " >= " + 0, - range.getOffset() >= 0); - assertTrue(range.getOffset() + " < " + input.length(), range - .getOffset() < input.length()); - assertTrue(range.getLength() + " <= " + input.length(), range - .getLength() <= input.length()); - assertTrue(range.getLength() + " > " + input.length(), range - .getLength() > 0); - } else { - System.out.println("Found untested types: " - + next.getClass().getSimpleName()); - } - } - } - - public void testSourceOffset() throws FormulaParseException { - final String input = "\u2200 x,y \u00b7 x=z+5+y"; - final int offset = 50; - - final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant(); - emfExpr.setPredicate(input); - TextPositionUtil.annotatePosition(emfExpr, offset - 10, - input.length() + 10); - - final TextRange subRange = TexttoolsFactory.eINSTANCE.createTextRange(); - subRange.setOffset(offset); - subRange.setLength(input.length()); - TextPositionUtil.addInternalPosition(emfExpr, input, subRange); - - FormulaResolver.resolve(emfExpr); - assertEquals(1, emfExpr.getExtensions().size()); - final AbstractExtension extension = emfExpr.getExtensions().get(0); - - final TreeIterator<EObject> iterator = EcoreUtil.getAllContents( - extension, false); - - while (iterator.hasNext()) { - final EObject next = iterator.next(); - - if (next instanceof BFormula) { - // test: every element has a position annotation - final BFormula formula = (BFormula) next; - final EAnnotation annotation = formula - .getEAnnotation(TextPositionUtil.ANNOTATION_TEXTRANGE); - assertNotNull(annotation); - } else if (next instanceof TextRange) { - // test: the position information is within the expected range - final TextRange range = (TextRange) next; - assertTrue(range.getOffset() + " >= " + offset, range - .getOffset() >= offset); - assertTrue(range.getOffset() + " < " + offset + input.length(), - range.getOffset() < offset + input.length()); - assertTrue(range.getLength() + " > " + 0, range.getLength() > 0); - assertTrue(range.getLength() + " <= " + input.length(), range - .getLength() <= input.length()); - } else if (!(next instanceof EAnnotation)) { - System.out.println("Found untested types: " - + next.getClass().getSimpleName()); - } - } - } -} diff --git a/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/CoreModelTest.java b/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/CoreModelTest.java deleted file mode 100644 index 6a91fa9..0000000 --- a/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/CoreModelTest.java +++ /dev/null @@ -1,22 +0,0 @@ -package org.eventb.texttools.internal.parsing; - -import junit.framework.TestCase; - -import org.eclipse.emf.common.util.EList; -import org.eventb.emf.core.machine.Machine; -import org.eventb.emf.core.machine.MachineFactory; - -public class CoreModelTest extends TestCase { - - public void testRefinesNames() throws Exception { - Machine machine = MachineFactory.eINSTANCE.createMachine(); - EList<String> list = machine.getRefinesNames(); - - list.add(0, "AbstractMac3"); - list.add(0, "AbstractMac2"); - list.add(0, "AbstractMac1"); - - assertEquals(3, machine.getRefinesNames().size()); - assertEquals(3, machine.getRefines().size()); - } -} diff --git a/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/TransformationVisitorTest.java b/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/TransformationVisitorTest.java deleted file mode 100644 index 07e33ab..0000000 --- a/org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/TransformationVisitorTest.java +++ /dev/null @@ -1,246 +0,0 @@ -package org.eventb.texttools.internal.parsing; - -import junit.framework.TestCase; - -import org.eclipse.emf.common.util.EList; -import org.eclipse.jface.text.Document; -import org.eclipse.jface.text.IDocument; -import org.eventb.emf.core.machine.Action; -import org.eventb.emf.core.machine.Convergence; -import org.eventb.emf.core.machine.Event; -import org.eventb.emf.core.machine.Guard; -import org.eventb.emf.core.machine.Invariant; -import org.eventb.emf.core.machine.Machine; -import org.eventb.emf.core.machine.Parameter; -import org.eventb.emf.core.machine.Variable; -import org.eventb.texttools.TextPositionUtil; -import org.eventb.texttools.model.texttools.TextRange; - -import de.be4.eventb.core.parser.BException; -import de.be4.eventb.core.parser.EventBParser; -import de.be4.eventb.core.parser.node.Start; - -public class TransformationVisitorTest extends TestCase { - - public void testMachineWithVariablesAndComments() throws BException { - final String input = "machine Test variables\n" + "varA varB\n" - + "/*varC\n" + "comment*/" + "varC\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - assertEquals("Test", machine.getName()); - assertEquals(0, machine.getRefinesNames().size()); - assertEquals(0, machine.getSees().size()); - - final EList<Variable> variables = machine.getVariables(); - assertEquals(3, variables.size()); - - Variable variable = variables.get(0); - assertNull(variable.getComment()); - assertEquals("varA", variable.getName()); - - variable = variables.get(1); - assertEquals("varC\n" + "comment", variable.getComment()); - assertEquals("varB", variable.getName()); - - variable = variables.get(2); - assertNull(variable.getComment()); - assertEquals("varC", variable.getName()); - } - - public void testMachineWithInvariantsAndComments() throws BException { - final String input = "machine Test invariants\n" + "@inv1 1=1\n" - + "/*inv2\n" + "comment*/" + "@inv2 2=2\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - assertEquals("Test", machine.getName()); - assertEquals(0, machine.getRefinesNames().size()); - assertEquals(0, machine.getSees().size()); - assertEquals(0, machine.getVariables().size()); - - final EList<Invariant> invariants = machine.getInvariants(); - assertEquals(2, invariants.size()); - - Invariant invariant = invariants.get(0); - assertEquals("inv2\n" + "comment", invariant.getComment()); - assertEquals("inv1", invariant.getName()); - assertEquals("1=1", invariant.getPredicate()); - - invariant = invariants.get(1); - assertNull(invariant.getComment()); - assertEquals("inv2", invariant.getName()); - assertEquals("2=2", invariant.getPredicate()); - } - - public void testTheorems() throws BException { - final String input = "machine Test invariants\n" + "@inv1 1=1\n" - + "theorem @inv2 2=2\n" + "@inv3 3=3\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - final EList<Invariant> invariants = machine.getInvariants(); - assertEquals(3, invariants.size()); - - Invariant invariant = invariants.get(0); - assertNull(invariant.getComment()); - assertEquals("inv1", invariant.getName()); - assertEquals("1=1", invariant.getPredicate()); - - invariant = invariants.get(1); - assertNull(invariant.getComment()); - assertEquals("inv2", invariant.getName()); - assertEquals("2=2", invariant.getPredicate()); - assertTrue(invariant.isTheorem()); - - invariant = invariants.get(2); - assertNull(invariant.getComment()); - assertEquals("inv3", invariant.getName()); - assertEquals("3=3", invariant.getPredicate()); - } - - public void testMachineWithEvents() throws BException { - final String input = "machine Test\n" + "refines MacA MacB\n" - + "events\n" + "ordinary event evt1\n" + "any a\n" - + "where @grd1 a=1\n" + "then\n" + "@act1 a≔1\n" + "end\n" - + "\n" + "anticipated event evt2\n" + "refines evtAbstract\n" - + "any b\n" + "with @x b=x\n" + "then\n" + "@act1 b≔1\n" - + "end\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - assertEquals("Test", machine.getName()); - assertEquals(2, machine.getRefinesNames().size()); - assertEquals("MacA", machine.getRefinesNames().get(0)); - assertEquals("MacB", machine.getRefinesNames().get(1)); - assertEquals(0, machine.getSees().size()); - assertEquals(0, machine.getVariables().size()); - - final EList<Event> events = machine.getEvents(); - assertEquals(2, events.size()); - - Event event = events.get(0); - assertNull(event.getComment()); - assertEquals("evt1", event.getName()); - assertEquals(Convergence.ORDINARY, event.getConvergence()); - final EList<Parameter> parameters = event.getParameters(); - assertEquals(1, parameters.size()); - assertNull(parameters.get(0).getComment()); - assertEquals("a", parameters.get(0).getName()); - final EList<Guard> guards = event.getGuards(); - assertEquals(1, guards.size()); - assertNull(guards.get(0).getComment()); - assertEquals("grd1", guards.get(0).getName()); - assertEquals("a=1", guards.get(0).getPredicate()); - final EList<Action> actions = event.getActions(); - assertEquals(1, actions.size()); - assertNull(actions.get(0).getComment()); - assertEquals("act1", actions.get(0).getName()); - assertEquals("a≔1", actions.get(0).getAction()); - - event = events.get(1); - assertEquals("evt2", event.getName()); - } - - public void testEventRefinement() throws BException { - final String input = "machine Test\n" + "events\n" + "event evt1\n" - + "end\n" + "\n" + "event evt2\n" + "refines evtX evtY\n" - + "end\n" + "event evt3\n" + "extends evtZ\n" + "end\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - final EList<Event> events = machine.getEvents(); - assertEquals(3, events.size()); - - Event event = events.get(0); - assertEquals("evt1", event.getName()); - assertEquals(Convergence.ORDINARY, event.getConvergence()); - assertEquals(0, event.getRefinesNames().size()); - assertFalse(event.isExtended()); - - event = events.get(1); - assertEquals("evt2", event.getName()); - assertEquals(Convergence.ORDINARY, event.getConvergence()); - assertEquals(2, event.getRefinesNames().size()); - assertFalse(event.isExtended()); - - event = events.get(2); - assertEquals("evt3", event.getName()); - assertEquals(Convergence.ORDINARY, event.getConvergence()); - assertEquals(1, event.getRefinesNames().size()); - assertTrue(event.isExtended()); - } - - public void testPositions() throws BException { - final String input = "machine Test\n" + "events\n" + "event X\n" - + "any Y\n" + "end\n" + "\n" + "event Y\n" + "refines X\n" - + "end\n" + "end"; - final Start rootNode = parseInput(input, false); - - final TransformationVisitor visitor = new TransformationVisitor(); - final IDocument document = new Document(input); - final Machine machine = visitor.transform(rootNode, document); - - final EList<Event> events = machine.getEvents(); - assertEquals(2, events.size()); - - Event event = events.get(0); - final TextRange eventRange1 = TextPositionUtil.getTextRange(event); - assertNotNull(eventRange1); - - final EList<Parameter> parameters = event.getParameters(); - assertEquals(1, parameters.size()); - final Parameter parameter = event.getParameters().get(0); - final TextRange paramRange = TextPositionUtil.getTextRange(parameter); - final TextRange stringRange1 = TextPositionUtil.getInternalPosition( - parameter, parameter.getName()); - - assertNotNull(paramRange); - assertNotNull(stringRange1); - assertNotSame(eventRange1, paramRange); - assertNotSame(paramRange, stringRange1); - - assertSame(stringRange1, TextPositionUtil.getInternalPosition( - parameter, parameter.getName())); - assertEquals(paramRange.getOffset(), stringRange1.getOffset()); - assertEquals(paramRange.getLength(), stringRange1.getLength()); - - event = events.get(1); - final TextRange eventRange2 = TextPositionUtil.getTextRange(event); - assertNotNull(eventRange2); - - final EList<String> refinesNames = event.getRefinesNames(); - assertEquals(1, refinesNames.size()); - - final TextRange refinesRange = TextPositionUtil.getInternalPosition( - event, refinesNames.get(0)); - assertNotNull(refinesRange); - - assertNotSame(eventRange2, refinesRange); - assertSame(refinesRange, TextPositionUtil.getInternalPosition(event, - refinesNames.get(0))); - assertTrue(refinesRange.getOffset() > eventRange2.getOffset()); - } - - private Start parseInput(final String input, final boolean debugOutput) - throws BException { - final EventBParser parser = new EventBParser(); - final Start rootNode = parser.parse(input, debugOutput); - return rootNode; - } -} diff --git a/org.eventb.texttools/.classpath b/org.eventb.texttools/.classpath index bd68a3e..03a0e29 100644 --- a/org.eventb.texttools/.classpath +++ b/org.eventb.texttools/.classpath @@ -1,10 +1,9 @@ <?xml version="1.0" encoding="UTF-8"?> <classpath> <classpathentry kind="src" path="src"/> - <classpathentry exported="true" kind="lib" path="lib/aspectjrt.jar"/> - <classpathentry exported="true" kind="lib" path="lib/EventBParser.jar" sourcepath="/de.be4.eventb.parser"/> - <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/> <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> + <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/> <classpathentry kind="src" path="src_generated"/> + <classpathentry kind="lib" path="lib/EventBParser.jar"/> <classpathentry kind="output" path="bin"/> </classpath> diff --git a/org.eventb.texttools/.project b/org.eventb.texttools/.project index 936ba24..f73953e 100644 --- a/org.eventb.texttools/.project +++ b/org.eventb.texttools/.project @@ -1,34 +1,30 @@ <?xml version="1.0" encoding="UTF-8"?> <projectDescription> <name>org.eventb.texttools</name> - <comment></comment> - <projects> - </projects> + <comment/> + <projects/> + <natures> + <nature>org.eclipse.pde.PluginNature</nature> + <nature>org.eclipse.jdt.core.javanature</nature> + <nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature> + </natures> <buildSpec> <buildCommand> <name>org.eclipse.jdt.core.javabuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.ManifestBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.SchemaBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> <buildCommand> <name>org.eclipse.pde.api.tools.apiAnalysisBuilder</name> - <arguments> - </arguments> + <arguments/> </buildCommand> </buildSpec> - <natures> - <nature>org.eclipse.pde.PluginNature</nature> - <nature>org.eclipse.jdt.core.javanature</nature> - <nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature> - </natures> + <linkedResources/> </projectDescription> diff --git a/org.eventb.texttools/.settings/org.eclipse.jdt.core.prefs b/org.eventb.texttools/.settings/org.eclipse.jdt.core.prefs deleted file mode 100644 index 0178f55..0000000 --- a/org.eventb.texttools/.settings/org.eclipse.jdt.core.prefs +++ /dev/null @@ -1,12 +0,0 @@ -#Sun May 10 11:23:16 CEST 2009 -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5 -org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve -org.eclipse.jdt.core.compiler.compliance=1.5 -org.eclipse.jdt.core.compiler.debug.lineNumber=generate -org.eclipse.jdt.core.compiler.debug.localVariable=generate -org.eclipse.jdt.core.compiler.debug.sourceFile=generate -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error -org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.source=1.5 diff --git a/org.eventb.texttools/META-INF/MANIFEST.MF b/org.eventb.texttools/META-INF/MANIFEST.MF index 7308635..e229a1e 100644 --- a/org.eventb.texttools/META-INF/MANIFEST.MF +++ b/org.eventb.texttools/META-INF/MANIFEST.MF @@ -2,7 +2,7 @@ Manifest-Version: 1.0 Bundle-ManifestVersion: 2 Bundle-Name: Event-B EMF Texttools Bundle-SymbolicName: org.eventb.texttools;singleton:=true -Bundle-Version: 3.0.0.qualifier +Bundle-Version: 3.0.1.qualifier Bundle-Activator: org.eventb.texttools.TextToolsPlugin Require-Bundle: org.eclipse.jface.text;bundle-version="[3.6.0,4.0.0)", org.eventb.emf.formulas;bundle-version="[1.3.2,2.0.0)", @@ -11,7 +11,8 @@ Require-Bundle: org.eclipse.jface.text;bundle-version="[3.6.0,4.0.0)", org.eclipse.emf.compare;bundle-version="[1.2.2,2.0.0)", org.eclipse.emf.compare.diff;bundle-version="[1.2.2,2.0.0)", org.eclipse.emf.compare.match;bundle-version="[1.2.2,2.0.0)", - org.eclipse.core.resources;bundle-version="[3.8.1,4.0.0)";visibility:=reexport + org.eclipse.core.resources;bundle-version="[3.8.1,4.0.0)";visibility:=reexport, + org.eclipse.emf.ecore Bundle-ActivationPolicy: lazy Bundle-RequiredExecutionEnvironment: J2SE-1.5 Export-Package: de.be4.eventb.core.parser.node, @@ -21,7 +22,6 @@ Export-Package: de.be4.eventb.core.parser.node, org.eventb.texttools.model.texttools, org.eventb.texttools.prettyprint, org.eventb.texttools.syntaxExtension -Bundle-ClassPath: lib/aspectjrt.jar, - lib/EventBParser.jar, +Bundle-ClassPath: lib/EventBParser.jar, . Bundle-Vendor: Heinrich-Heine University Dusseldorf diff --git a/org.eventb.texttools/build.properties b/org.eventb.texttools/build.properties index 2edb91d..47c27d0 100644 --- a/org.eventb.texttools/build.properties +++ b/org.eventb.texttools/build.properties @@ -4,7 +4,5 @@ output.. = bin/ bin.includes = META-INF/,\ .,\ plugin.xml,\ - lib/EventBParser.jar,\ - lib/aspectjrt.jar -src.includes = lib/EventBParser.jar,\ - lib/aspectjrt.jar + lib/EventBParser.jar +src.includes = lib/EventBParser.jar diff --git a/org.eventb.texttools/pom.xml b/org.eventb.texttools/pom.xml new file mode 100644 index 0000000..7386478 --- /dev/null +++ b/org.eventb.texttools/pom.xml @@ -0,0 +1,19 @@ +<?xml version="1.0" encoding="UTF-8"?> + <project + xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"> + <modelVersion>4.0.0</modelVersion> + + <parent> + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texteditor.parent</artifactId> + <version>1.0.0.qualifier</version> + <relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath> + </parent> + + <groupId>org.eventb.texteditor</groupId> + <artifactId>org.eventb.texttools</artifactId> + <version>3.0.1.qualifier</version> + <packaging>eclipse-plugin</packaging> + + </project> + \ No newline at end of file diff --git a/org.eventb.texttools/src/org/eventb/texttools/diff/EventBAttributesCheck.java b/org.eventb.texttools/src/org/eventb/texttools/diff/EventBAttributesCheck.java index 9817c8c..0ad5e9d 100755 --- a/org.eventb.texttools/src/org/eventb/texttools/diff/EventBAttributesCheck.java +++ b/org.eventb.texttools/src/org/eventb/texttools/diff/EventBAttributesCheck.java @@ -48,21 +48,14 @@ public class EventBAttributesCheck extends AttributesCheck { //ignore contents of string 2 string map entries (e.g. in RodinInternalDetails) // FIXME: make this more specific to RodinInternalDetails ignore = ignore || (container instanceof ENamedElement && "StringToStringMapEntry".equals(((ENamedElement) container).getName())); - //ignore contents of Annotations // FIXME: make this more specific to RodinInternalDetails ignore = ignore || container.equals(CorePackage.eINSTANCE.getAnnotation()); //ignore reference (instead, the derived attribute 'name' will be shown) ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_Reference()); - //ignore generated and local generated attributes as these must be preserved - ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_Generated()); //ADDED - ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_LocalGenerated()); //ADDED //ignore attributes of Abstract Extension ignore = ignore || container.equals(CorePackage.eINSTANCE.getAbstractExtension()); - //ignore attributes of Extension - ignore = ignore || container.equals(CorePackage.eINSTANCE.getExtension()); //ADDED - return ignore; } diff --git a/org.eventb.texttools/src/org/eventb/texttools/diff/EventBReferencesCheck.java b/org.eventb.texttools/src/org/eventb/texttools/diff/EventBReferencesCheck.java index b510054..0c6cf72 100755 --- a/org.eventb.texttools/src/org/eventb/texttools/diff/EventBReferencesCheck.java +++ b/org.eventb.texttools/src/org/eventb/texttools/diff/EventBReferencesCheck.java @@ -28,7 +28,6 @@ import org.eclipse.emf.ecore.EReference; import org.eclipse.emf.ecore.EcorePackage; import org.eclipse.emf.ecore.util.EcoreUtil.CrossReferencer; import org.eventb.emf.core.CorePackage; -import org.eventb.emf.core.machine.MachinePackage; public class EventBReferencesCheck extends ReferencesCheck { @@ -87,13 +86,12 @@ public class EventBReferencesCheck extends ReferencesCheck { ignore = ignore || reference.isContainer(); ignore = ignore || reference.eContainer().equals(EcorePackage.eINSTANCE.getEGenericType()); String name = reference.getName(); - // ignore = ignore || MachinePackage.eINSTANCE.getMachine_Refines() == reference; //Would this be a better way to check references rather than comparing names? ignore = ignore || "refines".equals(name); ignore = ignore || "sees".equals(name); ignore = ignore || "extends".equals(name); ignore = ignore || "annotations".equals(name); ignore = ignore || "extensions".equals(name); - //ignore = ignore || "attributes".equals(name); //Cannot ignore generic attributes since camille timestamp is an attribute + // ignore = ignore || "attributes".equals(name); //Cannot ignore generic attributes since camille timestamp is an attribute ignore = ignore || reference.eContainer().equals(CorePackage.eINSTANCE.getAnnotation()); return ignore; diff --git a/org.eventb.texttools/src/org/eventb/texttools/internal/parsing/TransformationVisitor.java b/org.eventb.texttools/src/org/eventb/texttools/internal/parsing/TransformationVisitor.java index 1383d5e..6d415d8 100644 --- a/org.eventb.texttools/src/org/eventb/texttools/internal/parsing/TransformationVisitor.java +++ b/org.eventb.texttools/src/org/eventb/texttools/internal/parsing/TransformationVisitor.java @@ -25,6 +25,7 @@ import org.eventb.emf.core.context.ContextFactory; import org.eventb.emf.core.machine.Action; import org.eventb.emf.core.machine.Convergence; import org.eventb.emf.core.machine.Event; +import org.eventb.emf.core.machine.Guard; import org.eventb.emf.core.machine.Invariant; import org.eventb.emf.core.machine.Machine; import org.eventb.emf.core.machine.MachineFactory; @@ -42,6 +43,7 @@ import de.be4.eventb.core.parser.node.AConstant; import de.be4.eventb.core.parser.node.AContextParseUnit; import de.be4.eventb.core.parser.node.AConvergentConvergence; import de.be4.eventb.core.parser.node.ADerivedAxiom; +import de.be4.eventb.core.parser.node.ADerivedGuard; import de.be4.eventb.core.parser.node.ADerivedInvariant; import de.be4.eventb.core.parser.node.AEvent; import de.be4.eventb.core.parser.node.AExtendedEventRefinement; @@ -261,6 +263,13 @@ public class TransformationVisitor extends DepthFirstAdapter { handleLabeledPredicate(MachineFactory.eINSTANCE.createGuard(), node, node.getPredicate(), node.getName(), node.getComments(), true); } + + @Override + public void outADerivedGuard(final ADerivedGuard node) { + Guard guard = MachineFactory.eINSTANCE.createGuard(); + guard.setTheorem(true); + handleLabeledPredicate(guard, node, node.getPredicate(), node.getName(), node.getComments(), true); + } @Override public void outAParameter(final AParameter node) { diff --git a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/ContextPrintSwitch.java b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/ContextPrintSwitch.java index 0994490..066f168 100644 --- a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/ContextPrintSwitch.java +++ b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/ContextPrintSwitch.java @@ -49,12 +49,12 @@ public class ContextPrintSwitch extends ContextSwitch<Boolean> implements final boolean newLine = (Boolean) printer.getPreference( PROP_NEWLINE_BETWEEN_CLAUSES, true); - // constants - printer.appendNameList(object.getConstants(), CONSTANTS, newLine); - // sets printer.appendNameList(object.getSets(), SETS, newLine); + // constants + printer.appendNameList(object.getConstants(), CONSTANTS, newLine); + // axioms printAxioms(object.getAxioms(), newLine); -- GitLab