From 139edf9ff230738133fab47173dd19d4591a3cdb Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 7 Dec 2023 16:41:32 +0100
Subject: [PATCH] Match only based on Event-B names and qualified references,
not EMF IDs
We don't care about generic EMF objects, only about EventBElement
(right..?). This noticeably improves performance when saving (almost
twice as fast for a medium-sized machine with 30 invariants).
---
org.eventb.texteditor.feature/feature.xml | 1 +
.../diffmerge/EventBEObjectMatcher.java | 50 ++++++-------------
2 files changed, 16 insertions(+), 35 deletions(-)
diff --git a/org.eventb.texteditor.feature/feature.xml b/org.eventb.texteditor.feature/feature.xml
index 43e54d3..c9827f8 100644
--- a/org.eventb.texteditor.feature/feature.xml
+++ b/org.eventb.texteditor.feature/feature.xml
@@ -9,6 +9,7 @@
<description>
A text editor for the Rodin platform to edit Event-B models
--- Release History ---
+3.6.0 - Improved performance when saving larger files.
3.5.1 - Fix "Empty label" error when adding a variant to a machine
3.5.0 - Compatibility with EventB-EMF 7.0.0 - fixes CamilleX dependency conflict. Fixed OOM error when top-level end keyword is missing.
3.4.1 - Internal updates to the build process - no visible changes.
diff --git a/org.eventb.texttools/src/org/eventb/texttools/diffmerge/EventBEObjectMatcher.java b/org.eventb.texttools/src/org/eventb/texttools/diffmerge/EventBEObjectMatcher.java
index 546d694..a46c8d5 100644
--- a/org.eventb.texttools/src/org/eventb/texttools/diffmerge/EventBEObjectMatcher.java
+++ b/org.eventb.texttools/src/org/eventb/texttools/diffmerge/EventBEObjectMatcher.java
@@ -12,10 +12,7 @@ import org.eclipse.emf.compare.Comparison;
import org.eclipse.emf.compare.Match;
import org.eclipse.emf.compare.match.eobject.IEObjectMatcher;
import org.eclipse.emf.ecore.EObject;
-import org.eclipse.emf.ecore.InternalEObject;
-import org.eclipse.emf.ecore.resource.Resource;
-import org.eclipse.emf.ecore.util.EcoreUtil;
-import org.eclipse.emf.ecore.xmi.XMIResource;
+import org.eventb.emf.core.EventBElement;
import org.eventb.emf.core.EventBNamed;
import org.eventb.emf.core.machine.Variant;
@@ -76,7 +73,8 @@ public class EventBEObjectMatcher implements IEObjectMatcher {
return false;
}
/*
- * Only one variant may exist in a model, so two variants are a match
+ * Only one variant may exist in a model, so two variants are a match.
+ * TODO Rodin now allows multiple variants per model, but Camille doesn't support that properly yet...
*/
if (left instanceof Variant) {
assert candidate instanceof Variant;
@@ -84,51 +82,33 @@ public class EventBEObjectMatcher implements IEObjectMatcher {
}
/*
- * Improve matching for event b named objects with same name
+ * Match named elements based on only their name and not their fully qualified reference,
+ * so that renaming a component doesn't cause mismatches for all the elements in it.
*/
if (left instanceof EventBNamed) {
assert candidate instanceof EventBNamed;
EventBNamed l = (EventBNamed) left;
EventBNamed c = (EventBNamed) candidate;
- if (l.getName().equals(c.getName())) {
- return true;
- }
+ return l.getName().equals(c.getName());
}
/*
- * rely on emf identifiers after the event-b specific code
+ * Match unnamed objects based on their fully qualified reference,
+ * which includes a unique ID generated by Event-B EMF.
*/
- String idLeft = getEMFId(left);
- if (idLeft == null) {
- return false;
+ if (left instanceof EventBElement) {
+ assert candidate instanceof EventBElement;
+ EventBElement l = (EventBElement)left;
+ EventBElement c = (EventBElement)candidate;
+ return l.getReference().equals(c.getReference());
}
- String idCandidate = getEMFId(candidate);
- return idLeft.equals(idCandidate);
+
+ return false;
}
private static boolean areSameType(final EObject obj1, final EObject obj2) {
return obj1 != null && obj2 != null
&& obj1.eClass().equals(obj2.eClass());
}
-
- private static String getEMFId(EObject eObject) {
- final String identifier;
- if (eObject.eIsProxy()) {
- identifier = ((InternalEObject) eObject).eProxyURI().fragment();
- } else {
- String functionalId = EcoreUtil.getID(eObject);
- if (functionalId != null) {
- identifier = functionalId;
- } else {
- final Resource eObjectResource = eObject.eResource();
- if (eObjectResource instanceof XMIResource) {
- identifier = ((XMIResource) eObjectResource).getID(eObject);
- } else {
- identifier = null;
- }
- }
- }
- return identifier;
- }
}
--
GitLab