From ffb7fb79e64df8054608ec5af0e21bdc4709c350 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Wed, 25 Jun 2025 13:34:34 +0200 Subject: [PATCH] Fix indents --- .../translator/internal/ModelTranslator.java | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java index 094bac9f..c9ab015d 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java @@ -581,19 +581,19 @@ public class ModelTranslator extends AbstractComponentTranslator { final PPredicate predicate = translatePredicate(ff, te, evPredicate); if (evPredicate.getSource() instanceof IInvariant) { // test can fail for generated invariants - final IInvariant ucp = (IInvariant) evPredicate.getSource(); // comments only attached in unchecked source - if (ucp.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) { - final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE); - //System.out.println("Invariant/theorem " + predicate + " has description " + commentString); - final TPragmaFreeText desc = new TPragmaFreeText(commentString); - ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc)); - ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate); - list.add(dpred); - labelMapping.put(dpred, evPredicate); - } else { - list.add(predicate); - labelMapping.put(predicate, evPredicate); - } + final IInvariant ucp = (IInvariant) evPredicate.getSource(); // comments only attached in unchecked source + if (ucp.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) { + final String commentString = ucp.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE); + //System.out.println("Invariant/theorem " + predicate + " has description " + commentString); + final TPragmaFreeText desc = new TPragmaFreeText(commentString); + ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc)); + ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate); + list.add(dpred); + labelMapping.put(dpred, evPredicate); + } else { + list.add(predicate); + labelMapping.put(predicate, evPredicate); + } } else { // cannot cast source to IInvariant list.add(predicate); labelMapping.put(predicate, evPredicate); @@ -614,7 +614,7 @@ public class ModelTranslator extends AbstractComponentTranslator { final String srcName = src.getRodinFile().getBareName(); result = currentName.equals(srcName); } else { - // Some plugins virtually add new invariants (e.g., FOLLOWED_BY for events) + // Some plugins virtually add new invariants (e.g., FOLLOWED_BY for events) Logger.notifyUser("Source of invariant in " + currentName + " is not a machine. Invariant may be added multiple times."); // TODO: check if this source is local or not result = false; // assume it is local so that it is added in the translation -- GitLab