From 7ea65073f76fd3981c8f36848de0d74c22b0de9a Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 6 Dec 2023 16:22:45 +0100
Subject: [PATCH] Log exceptions in applyDiff instead of just printing them to
stdout
This way they are visible to normal users.
---
.../src/org/eventb/texttools/PersistenceHelper.java | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java b/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java
index a5b819d..4617d4a 100644
--- a/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java
+++ b/org.eventb.texttools/src/org/eventb/texttools/PersistenceHelper.java
@@ -167,8 +167,8 @@ public class PersistenceHelper {
try {
if (d.getState() != DifferenceState.MERGED)
evbMerger.copyRightToLeft(d,null);
- } catch(Exception e) {
- System.out.println("SKIPED:"+d);
+ } catch (RuntimeException e) {
+ TextToolsPlugin.getDefault().getLog().error("Failed to apply diff while saving edit", e);
}
}
--
GitLab