diff --git a/build.gradle b/build.gradle index 6c3da432c954fab0d4d01b140b1228fc5f5a786b..334de54b64d7d4d04d6b2f1c73e0efa520f1b227 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 03bdf1281a62f8b20a8080d2dc33190e56b5a1ec..ee74eee56f6a5923d5d9ee09eb2b8d30fd54a29e 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 7e6dbbccaf8c0c3b3bfa4cb616079e422fd83f8d..4424182a419114abb07f3430fb20d18244e9c30d 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 39f590a186343dee651ab1d5a720ababf98d3eb9..bfd2f09f82d0b249167e523a5f9a2a2500de1669 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 21c0f419e8ad90eabb0e2acb96a16c5440b89465..f0b86471d96fe7010361c98a8bab788203ecccd1 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 a6ee876dc262fd836ac699cf16cfd96c9067c012..7e70966622ceb33de39ce65a2914c1e0044693bb 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 6af7bc8b66229828ae1520a1de2a6e2b297a30e3..d9b7487204ad273df1547cfdde658b5738af92c4 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 267850d5ece130b517dcc9160ca9d80ca6e48eb1..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..fb884b4c116d82c4987ea243d8b3e7c80b7521e6 --- /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 397bf70082bb74a5c6494a551f1510adbced1bfb..908418bcd77ed5920a3a59cbafc99817e8ca2ebc 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 cc5ef6991da5475b940cf70808b1ff3e7260fea1..c5bb45432ab941c41f76cd9da72eea66a1d4361a 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 b510d1117b56169437291798cf0efbfbbc71964b..5c04d5c68544b46d822f5419d75cff6315f65d57 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 0000000000000000000000000000000000000000..e6e12536e5f71fae41fa5f95d4294bfb8db6cea0 --- /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 3f45abbb08d87e2f4aa2a5719974742810befd87..1f55a9afadf62fd9705bbc017d966b93598d067a 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 0000000000000000000000000000000000000000..db190cbdedbeada73660e5169c3c600a61a5ef65 --- /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 0000000000000000000000000000000000000000..7959d136a07687f5ec8003abd8788f66b4b6f435 --- /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 0000000000000000000000000000000000000000..11959749314ba7dd8e5e817f631208d6f8836381 --- /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 0000000000000000000000000000000000000000..fca084df10183d595acfb35765ae1b405f678ebe --- /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 cdf77e53eb0c88a3e3b0dba86a5a4f67137572a6..ad4b38cb3f3926d0413260d0ad7d739a89efd97b 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 f4c75c1f6b72a7280918a29c18c2623a122b7153..2a06124005f40721fab008d8714dc605e3598e11 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 bb1930094c1824baf52a0d8ba07d7ba68c17472f..0000000000000000000000000000000000000000 --- 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 75021432d7b9573b0b7e35bf994a6c15a34947e1..647006800899ef87d41ae9c0059f702061100e9d 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 0000000000000000000000000000000000000000..6e281228a91bb9e310c05be475d3bf42c0cff283 --- /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 5e4c1fe99cf222cf9ea3b58fdef54017f533360d..0000000000000000000000000000000000000000 --- 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 36c1ac73129c0cb9cfc1ab039c3d134363d53535..0000000000000000000000000000000000000000 --- 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 8cbaba212c35b17bca4f2286b131fb4cbfd0460e..0000000000000000000000000000000000000000 --- 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 34d2e4d2dad529ceaeb953bfcdb63c51d69ffed2..0000000000000000000000000000000000000000 --- 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 00614bee5fb2f9eccd13c310234a59245a157d0a..0000000000000000000000000000000000000000 --- 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 a0f51096b940cb123dcaaca160c111ffc5194ffc..0000000000000000000000000000000000000000 --- 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 c6999d5518a70cf6d11ff06c99c6c1532d78be23..0000000000000000000000000000000000000000 --- 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 6a91fa956ea880b06164bb413f58d9d916796735..0000000000000000000000000000000000000000 --- 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 07e33ab5e75eeca75d29de6338b5b00a161d6ed2..0000000000000000000000000000000000000000 --- 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 bd68a3e21618f25ae1009e76f998df4d70851106..03a0e297310cc4dd6f8b7ddad72d1b555ac4f35e 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 936ba24962a14bd8ff48500da35b74f50b4e1d99..f73953e90fdfa6a9474a22d855f4fe471a7dc310 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 0178f55888c2ce9819b5d9864de0938aa301633d..0000000000000000000000000000000000000000 --- 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 7308635be00d7fd839557af9a80251877efbb15e..e229a1e618b1e3bb070f970d7f135fae8fd466d1 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 2edb91ddd1a5e4288c5e0e3b412b6bfe9d3f7780..47c27d05b203a9f88618c8eca3da7814f7e0a67d 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 0000000000000000000000000000000000000000..738647882146db4837821d481a1c4358ec7290b8 --- /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 9817c8c7c436039b31f904bbe49815daa5c96154..0ad5e9d13e1404ff1b90c5d5cf0f758807ffdf56 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 b510054996283093847ebbfb3ff517b9c2b59c9f..0c6cf72dfefbcbfb23d5f9ee24074b0bc3310ac0 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 1383d5e4fa4089b184d68a24e5cecdd72b87afc7..6d415d8a9549af6a1d379eb69e0230c2471a1851 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 099449082ca670547991a08c33d434e9983e5515..066f1689b9cec8951119e22c688934f1c8e43592 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);