Skip to content
Snippets Groups Projects
Commit 708d4ac6 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

export comments of variables as description pragmas

parent 68f3cb26
No related branches found
No related tags found
No related merge requests found
Pipeline #145717 passed
...@@ -37,6 +37,7 @@ import org.eventb.core.ISCVariable; ...@@ -37,6 +37,7 @@ import org.eventb.core.ISCVariable;
import org.eventb.core.ISCVariant; import org.eventb.core.ISCVariant;
import org.eventb.core.ISCWitness; import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement; import org.eventb.core.ITraceableElement;
import org.eventb.core.IVariable;
import org.eventb.core.IVariant; import org.eventb.core.IVariant;
import org.eventb.core.ast.Assignment; import org.eventb.core.ast.Assignment;
import org.eventb.core.ast.FormulaFactory; import org.eventb.core.ast.FormulaFactory;
...@@ -52,6 +53,7 @@ import org.rodinp.core.RodinDBException; ...@@ -52,6 +53,7 @@ import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus; import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus;
import de.be4.classicalb.core.parser.node.AConvergentEventstatus; import de.be4.classicalb.core.parser.node.AConvergentEventstatus;
import de.be4.classicalb.core.parser.node.ADescriptionEvent; import de.be4.classicalb.core.parser.node.ADescriptionEvent;
import de.be4.classicalb.core.parser.node.ADescriptionExpression;
import de.be4.classicalb.core.parser.node.ADescriptionPragma; import de.be4.classicalb.core.parser.node.ADescriptionPragma;
import de.be4.classicalb.core.parser.node.ADescriptionPredicate; import de.be4.classicalb.core.parser.node.ADescriptionPredicate;
import de.be4.classicalb.core.parser.node.AEvent; import de.be4.classicalb.core.parser.node.AEvent;
...@@ -452,9 +454,19 @@ public class ModelTranslator extends AbstractComponentTranslator { ...@@ -452,9 +454,19 @@ public class ModelTranslator extends AbstractComponentTranslator {
variable.getIdentifierString()); variable.getIdentifierString());
final AIdentifierExpression id = new AIdentifierExpression( final AIdentifierExpression id = new AIdentifierExpression(
Arrays.asList(new TIdentifierLiteral[] { literal })); Arrays.asList(new TIdentifierLiteral[] { literal }));
final IVariable ucv = (IVariable) variable.getSource(); // comments only attached in unchecked source
if (ucv.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
final String commentString = ucv.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
final ADescriptionExpression descid = new ADescriptionExpression(descPragma,id);
list.add(descid);
} else {
list.add(id); list.add(id);
} }
} }
}
variablesModelClause.setIdentifiers(list); variablesModelClause.setIdentifiers(list);
return variablesModelClause; return variablesModelClause;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment