diff --git a/key.core/src/main/antlr4/JavaKeYLexer.g4 b/key.core/src/main/antlr4/JavaKeYLexer.g4 index 9ea0ac834ee..6201035a43f 100644 --- a/key.core/src/main/antlr4/JavaKeYLexer.g4 +++ b/key.core/src/main/antlr4/JavaKeYLexer.g4 @@ -40,6 +40,7 @@ ISARRAY:'\\isArray'; ISARRAYLENGTH:'\\isArrayLength'; ISCONSTANT: '\\isConstant'; ISENUMTYPE:'\\isEnumType'; +ISENUMCONST:'\\isEnumConst'; ISINDUCTVAR:'\\isInductVar'; ISLOCALVARIABLE : '\\isLocalVariable'; ISOBSERVER : '\\isObserver'; diff --git a/key.core/src/main/antlr4/JavaKeYParser.g4 b/key.core/src/main/antlr4/JavaKeYParser.g4 index f7cbe0432d8..789d2f397a5 100644 --- a/key.core/src/main/antlr4/JavaKeYParser.g4 +++ b/key.core/src/main/antlr4/JavaKeYParser.g4 @@ -213,6 +213,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | SIMPLIFY_IF_THEN_ELSE_UPDATE | CONTAINS_ASSIGNMENT | ISENUMTYPE + | ISENUMCONST | ISTHISREFERENCE | STATICMETHODREFERENCE | ISREFERENCEARRAY diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/EnumClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/EnumClassDeclaration.java index aaf2a962488..6a8fb601cb9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/EnumClassDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/EnumClassDeclaration.java @@ -3,57 +3,70 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.ast.declaration; -import java.util.ArrayList; import java.util.List; +import java.util.Objects; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; -import de.uka.ilkd.key.logic.JavaDLFieldNames; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; + +import com.github.javaparser.ast.body.EnumConstantDeclaration; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; /** * This class is used for wrapping an enum into a standard class type. * *

- * In addition the programvariables that represent enum constants are memorized. Thus this class is + * In addition, the programvariables that represent enum constants are memorized. Thus this class is * able to have queries on the enum constants. * + * mulbrich: Update 2025 (a mere 19 years later): + * Updated from the old heap model to the new one. + * * @author mulbrich - * @since 2006-12-10 + * @since 2006-12-10, updated 2025-10-24 by MU */ - +@NullMarked public class EnumClassDeclaration extends ClassDeclaration { + public record EnumEntry(String name, int ordinal, IProgramVariable variable) { + } /** * store the program variables which represent the enum constants + * in a lookup map from name to (ordinal index, program variable) */ - private final List constants = new ArrayList<>(); + private final ImmutableList constants; /** * create a new EnumClassDeclaration that describes an enum defintion. It merely wraps a * ClassDeclaration but has memory about which fields have been declared as enum constants. * - * @param children - * children in the ast (members) - * @param fullName - * of the class/enum - * @param isLibrary - * see class constructor + * @param children children in the ast (members) + * @param fullName of the class/enum + * @param isLibrary see class constructor + * @param enumConstantDeclarations the declarations for the enum constants */ - // TODO javaparser public EnumClassDeclaration( - ExtList children, ProgramElementName fullName, boolean isLibrary - /* , List enumConstantDeclarations */) { + ExtList children, ProgramElementName fullName, boolean isLibrary, + List enumConstantDeclarations) { super(children, fullName, isLibrary); - // for (EnumConstantDeclaration ecd : enumConstantDeclarations) { - // String constName = ecd.getEnumConstantSpecification().getName(); - // constants.add(findAttr(constName)); - // } + ImmutableList seq = ImmutableSLList.nil(); + int ordinal = 0; + for (EnumConstantDeclaration ecd : enumConstantDeclarations) { + String constName = ecd.getNameAsString(); + seq = seq.prepend(new EnumEntry(constName, ordinal, findAttr(constName))); + ordinal++; + } + + constants = seq; } /* @@ -64,11 +77,12 @@ public EnumClassDeclaration( * */ private IProgramVariable findAttr(String fieldName) { - String completeName = getFullName() + JavaDLFieldNames.SEPARATOR + fieldName; + // TODO String completeName = getFullName() + JavaDLFieldNames.SEPARATOR + fieldName; + String completeName = getFullName() + "::" + fieldName; for (int i = 0; i < members.size(); i++) { if (members.get(i) instanceof FieldDeclaration fd) { FieldSpecification fs = fd.getFieldSpecifications().get(0); - if (fs.getName().equals(completeName)) { + if (Objects.equals(fs.getName(), completeName)) { return fs.getProgramVariable(); } } @@ -81,12 +95,7 @@ private IProgramVariable findAttr(String fieldName) { * is pv a enum constant of THIS enum? */ private boolean isLocalEnumConstant(IProgramVariable pv) { - for (IProgramVariable cnst : constants) { - if (cnst.equals(pv)) { - return true; - } - } - return false; + return constants.stream().anyMatch(it -> it.variable.equals(pv)); } /** @@ -98,7 +107,7 @@ private boolean isLocalEnumConstant(IProgramVariable pv) { */ private int localIndexOf(ProgramVariable pv) { for (int i = 0; i < constants.size(); i++) { - if (constants.get(i).equals(pv)) { + if (constants.get(i).variable.equals(pv)) { return i; } } @@ -142,4 +151,15 @@ public static int indexOf(ProgramVariable attribute) { } } + + /** + * get the constant with the given name, including its ordinal index. + * + * @param fieldName the name of the enum constant + * @return a pair of (index, program variable) of the enum constant with the given name or null + * if there is no such constant + */ + public @Nullable EnumEntry getConstant(String fieldName) { + return constants.stream().filter(it -> it.name == fieldName).findAny().orElse(null); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 4098d15a2c3..d2419c211a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -640,6 +640,7 @@ private boolean applyManipulator(boolean negated, Object[] args, manipulator.apply(peekTBuilder(), args, parameters, negated); return true; } catch (Throwable e) { + LOGGER.debug("Unexpected exception while producing variable condition", e); return false; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java index a5353a2ef01..b35352cfc0a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java @@ -10,7 +10,12 @@ import org.key_project.prover.rules.VariableCondition; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + public class ConstructorBasedBuilder extends AbstractConditionBuilder { + + private static final Logger LOGGER = LoggerFactory.getLogger(ConstructorBasedBuilder.class); private final Class clazz; private final boolean negationSupported; @@ -54,8 +59,14 @@ public VariableCondition build(Object[] arguments, List parameters, bool return (VariableCondition) constructor.newInstance(args); } catch (InstantiationException | IllegalAccessException | InvocationTargetException | IllegalArgumentException ignored) { + LOGGER.debug("Constructor " + constructor + + " does not match the given arguments for VariableCondition " + clazz + + ". Trying next constructor."); } } - throw new RuntimeException(); + + throw new RuntimeException( + "No matching constructor found for VariableCondition " + clazz + " with args " + + Arrays.toString(args)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 67065ce497c..19a9ef3d20c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -228,7 +228,7 @@ public void apply(TacletBuilder tb, Object[] arguments, List paramete public static final AbstractConditionBuilder FINAL = new ConstructorBasedBuilder("final", FinalReferenceCondition.class, SV); public static final AbstractConditionBuilder ENUM_CONST = - new ConstructorBasedBuilder("isEnumConst", EnumConstantCondition.class, SV); + new ConstructorBasedBuilder("isEnumConst", EnumConstantCondition.class, SORT, SV); public static final AbstractConditionBuilder LOCAL_VARIABLE = new ConstructorBasedBuilder("isLocalVariable", LocalVariableCondition.class, SV); public static final AbstractConditionBuilder ARRAY_LENGTH = @@ -260,8 +260,8 @@ public VariableCondition build(Object[] arguments, List parameters, return new TypeCondition((TypeResolver) arguments[0], !negated, non_null); } }; - public static final AbstractConditionBuilder ENUM_TYPE = - new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV); + // public static final AbstractConditionBuilder ENUM_TYPE = + // new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV); public static final AbstractConditionBuilder CONTAINS_ASSIGNMENT = new ConstructorBasedBuilder("containsAssignment", ContainsAssignmentCondition.class, SV); public static final AbstractConditionBuilder FIELD_TYPE = @@ -377,7 +377,7 @@ public IsLabeledCondition build(Object[] arguments, List parameters, FREE_3, FREE_4, FINAL_TYPE, FREE_5, NEW_TYPE_OF, NEW_DEPENDING_ON, FREE_LABEL_IN_VARIABLE, DIFFERENT, FINAL, ENUM_CONST, LOCAL_VARIABLE, ARRAY_LENGTH, ARRAY, REFERENCE_ARRAY, MAY_EXPAND_METHOD_2, - MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, ENUM_TYPE, + MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, /* ENUM_TYPE, */ CONTAINS_ASSIGNMENT, FIELD_TYPE, STATIC_REFERENCE, DIFFERENT_FIELDS, SAME_OBSERVER, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java index 0b099102d5c..7658ee9d698 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumConstantCondition.java @@ -5,34 +5,41 @@ import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.declaration.EnumClassDeclaration; -import de.uka.ilkd.key.java.ast.reference.FieldReference; -import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.SyntaxElement; +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Operator; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; /** - * ensures that the given instantiation for the schemavariable denotes a constant of an enum type. + * ensures that the given instantiation for the schema-variable denotes a constant of an enum type. * * @author mulbrich * @since 2006-12-04 * @version 2006-12-11 + * @version 2025-10-24 Refactored for the "new" heap model. */ public final class EnumConstantCondition extends VariableConditionAdapter { private final SchemaVariable reference; + private final GenericSort typeReference; /** * the static reference condition checks if a suggested instantiation for a schema variable * denotes a reference to an enum constant. */ - public EnumConstantCondition(SchemaVariable reference) { + public EnumConstantCondition(GenericSort typeReference, SchemaVariable reference) { this.reference = reference; + this.typeReference = typeReference; } @@ -41,27 +48,50 @@ public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations s Services services) { if (var == reference) { - // new ObjectInspector(var).setVisible(true); - // new ObjectInspector(subst).setVisible(true); - ProgramVariable progvar; - - if (subst instanceof FieldReference) { - progvar = ((FieldReference) subst).getProgramVariable(); - } else if (subst instanceof JTerm && ((JTerm) subst).op() instanceof ProgramVariable) { - progvar = (ProgramVariable) ((JTerm) subst).op(); - } else { + // try to find the enum constant field + EnumClassDeclaration.EnumEntry field = resolveEnumFieldConstant(subst, services); + if (field == null) return false; - } - - return EnumClassDeclaration.isEnumConstant(progvar); + // if there is such a field, check that its type is the right enum type + KeYJavaType containerType = ((ProgramVariable) field.variable()).getContainerType(); + Sort typeInst = svInst.getGenericSortInstantiations().getInstantiation(typeReference); + return containerType.getSort() == typeInst; } + return true; } + // also used in EnumConstantValue + public static EnumClassDeclaration.EnumEntry resolveEnumFieldConstant(Object obj, + Services services) { + if (obj instanceof Term term) { + Operator op = term.op(); + if (op instanceof Function func && func.isUnique() + && func.sort() == services.getTypeConverter().getHeapLDT().getFieldSort() + && func.name().toString().contains("::")) { + String funcName = func.name().toString(); + int colon = funcName.indexOf("::$"); + if (colon == -1) { + return null; + } + String sortName = funcName.substring(0, colon); + String fieldName = funcName.substring(colon + 3); + KeYJavaType kjt = services.getJavaInfo().getKeYJavaType(sortName); + if (kjt == null || !(kjt.getJavaType() instanceof EnumClassDeclaration ecd)) { + return null; + } + + return ecd.getConstant(fieldName); + } + } + return null; + } + + @Override public String toString() { - return "\\enumConstant(" + reference + ")"; + return "\\isEnumConst(" + typeReference + ", " + reference + ")"; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java index 5902cd8a987..8bb757f64c4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java @@ -19,9 +19,15 @@ /** * This variable condition checks if a type is an enum type. * + * @deprecated As of 2025, this varcond is no longer needed, its functionality is currently + * handled by {@link EnumConstantCondition} that checks type and constant field in one + * varcond. + * Should be removed soon. + * * @author mulbrich * @since 2006-12-14 */ +@Deprecated public final class EnumTypeCondition extends VariableConditionAdapter { private static final Logger LOGGER = LoggerFactory.getLogger(EnumTypeCondition.class); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java index a6031d61158..1e0a9882aba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java @@ -3,23 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.metaconstruct; -import de.uka.ilkd.key.java.KeYJavaASTFactory; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.declaration.EnumClassDeclaration; -import de.uka.ilkd.key.java.ast.expression.literal.IntLiteral; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.AbstractTermTransformer; -import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.rule.conditions.EnumConstantCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; -import org.key_project.logic.op.Operator; /** * resolve a program variable to an integer literal. * - * If the PV is a enum constant, its index in the enum constant array is returned. If the PC is a - * reference to the nextToCreate field than the number of enum constants is returned. + * If the PV is a enum constant field constant, its index in the enum constant array is returned. + * This is the ordinal of the enum constant. * * @author mulbrich */ @@ -39,33 +36,15 @@ public EnumConstantValue() { */ public JTerm transform(JTerm term, SVInstantiations svInst, Services services) { term = term.sub(0); - Operator op = term.op(); - if (op instanceof ProgramVariable pv) { - int value; - - // String varname = pv.getProgramElementName().getProgramName(); - - if (false) {// varname.endsWith(ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE)) {//TODO - // - if (pv.getContainerType().getJavaType() instanceof EnumClassDeclaration ecd) { - value = ecd.getNumberOfConstants(); - } else { - throw new IllegalArgumentException(term + " is not in an enum type."); - } - } else { - // enum constant - value = EnumClassDeclaration.indexOf(pv); - if (value == -1) { - throw new IllegalArgumentException(term + " is not an enum constant"); - } - } - - final IntLiteral valueLiteral = KeYJavaASTFactory.intLiteral(value); - term = services.getTypeConverter().convertToLogicElement(valueLiteral); + EnumClassDeclaration.EnumEntry enConst = + EnumConstantCondition.resolveEnumFieldConstant(term, services); + if (enConst == null) { + return term; } - return term; + int ordinal = enConst.ordinal(); + return services.getTermBuilder().zTerm(ordinal); } } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java index 2f822fc942a..7e26e6449c7 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Enum.java @@ -5,9 +5,13 @@ public abstract class Enum extends java.lang.Object implements java.lang.Comparable, java.io.Serializable { - public final java.lang.String name(); - public final int ordinal(); + + /*@ public normal_behavior + @ ensures \result == \dl_enumOrdinal(this); + @ assignable \strictly_nothing; + @*/ + public /*@ helper */ final int ordinal(); protected Enum(java.lang.String arg0, int arg1); public final java.lang.Class getDeclaringClass(); public static java.lang.Enum valueOf(java.lang.Class arg0, java.lang.String arg1); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key index 5db23d9e9d7..eb514ec2ead 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key @@ -3,10 +3,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ \sorts { - \generic E; + \generic E \extends java.lang.Object; \generic G; } +\functions { +} + \schemaVariables { \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal; \program Type #ty; @@ -25,7 +28,8 @@ \formula post, inv; - \term E e; + \term Field e; + \term Field e1, e2; } /*** @@ -72,25 +76,29 @@ *** Enumerations ***/ \rules(programRules:Java) { - /* XXX - enumConstantByIndex { - \assumes(wellFormed(heap) ==>) - \find( e ) - \sameUpdateLevel - \varcond(\enumConstant(e)) - \replacewith( E::(#enumconstantvalue(e)) ) + enumConstantEq { + \find( E::final(null, e1) = E::final(null, e2) ) + \varcond(\isEnumConst(E, e1), \isEnumConst(E, e2)) + \replacewith( e1 = e2 ) \heuristics(simplify) }; + enumConstantNull { + \find( E::final(null, e) = null ) + \varcond(\isEnumConst(E, e)) + \replacewith( false ) + \heuristics(simplify) + }; enumOrdinalToIndex { - \find( #fieldref(e, "ordinal") ) - \varcond(\isEnumType(E)) - \add(e = E::(#fieldref(e, "ordinal")) ==> ) + \find( enumOrdinal(E::final(null, e)) ) + \varcond(\isEnumConst(E, e)) + \replacewith( #enumconstantvalue(e) ) + \heuristics(simplify) }; +} - } - +/* \rules(programRules:Java,initialisation:disableStaticInitialisation) { enumNextToCreateConstant { @@ -114,5 +122,5 @@ \replacewith( #enumconstantvalue(#nc) ) \heuristics(simplify) }; - */ -} + + }*/ diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key index bd29c3dd874..fc03beadccd 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key @@ -34,4 +34,6 @@ /*! A boolean function which is true iff the dynamic type of its argument is a subtype of the type which is part of the function name. */ boolean instance<[alpha]>(any); + + int enumOrdinal(java.lang.Object); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index d561037db4c..dbd58a89f54 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -26,11 +26,11 @@ import de.uka.ilkd.key.gui.actions.SendFeedbackAction; import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.sourceview.JavaJMLEditorLexer; -import de.uka.ilkd.key.gui.sourceview.KeYEditorLexer; import de.uka.ilkd.key.gui.sourceview.SourceHighlightDocument; import de.uka.ilkd.key.gui.sourceview.TextLineNumber; import de.uka.ilkd.key.gui.utilities.ErrorMarkPainter; import de.uka.ilkd.key.gui.utilities.GuiUtilities; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.speclang.SLEnvInput; @@ -703,7 +703,8 @@ private void updatePreview(PositionedIssueString issue) { if (isJava(uri.getPath())) { showSourceCode(source, new JavaJMLEditorLexer()); } else if (isKeY(uri.getPath())) { - showSourceCode(source, new KeYEditorLexer()); + showSourceCode(source, + new LexerHighlighter.KeYLexerHighlighter().getEditorLexer()); } else { txtSource.setText(source); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index 7ae10693bf2..67dd66e91ec 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java @@ -22,10 +22,10 @@ import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.sourceview.JavaJMLEditorLexer; -import de.uka.ilkd.key.gui.sourceview.KeYEditorLexer; import de.uka.ilkd.key.gui.sourceview.SourceHighlightDocument; import de.uka.ilkd.key.gui.sourceview.TextLineNumber; import de.uka.ilkd.key.gui.utilities.CurrentLineHighlighter; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; import de.uka.ilkd.key.util.ExceptionTools; import org.key_project.util.java.IOUtil; @@ -179,7 +179,7 @@ public void addNotify() { if (file.toString().endsWith(".java")) { lexer = new JavaJMLEditorLexer(); } else if (file.toString().endsWith(".key") || file.toString().endsWith(".proof")) { - lexer = new KeYEditorLexer(); + lexer = new LexerHighlighter.KeYLexerHighlighter().getEditorLexer(); } else { lexer = SourceHighlightDocument.TRIVIAL_LEXER; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java deleted file mode 100644 index 52f7e8ed14c..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/KeYEditorLexer.java +++ /dev/null @@ -1,156 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.gui.sourceview; - -import java.awt.*; -import java.util.ArrayList; -import java.util.BitSet; -import java.util.List; -import javax.swing.text.SimpleAttributeSet; -import javax.swing.text.StyleConstants; - -import de.uka.ilkd.key.gui.colors.ColorSettings; -import de.uka.ilkd.key.nparser.JavaKeYLexer; - -import org.antlr.v4.runtime.CharStreams; - -import static de.uka.ilkd.key.nparser.JavaKeYLexer.*; - -/** - * This is a lexer class used by a {@link SourceHighlightDocument} to highlight KeY code. - * It uses the ANTLR lexer {@link JavaKeYLexer} to tokenize the text. - * - * Secondary keywords are highlighted in a different color. These are schema variables kinds, - * variable conditions etc. - * - * @author Mattias Ulbrich - */ -public class KeYEditorLexer implements SourceHighlightDocument.EditorLexer { - - /** highight color for KeY keywords (dark red/violet) */ - private static final ColorSettings.ColorProperty KEYWORD_COLOR = - ColorSettings.define("[key]keyword", "", new Color(0x7f0055)); - - /** highight color for secondary KeY keywords (light red/violet) */ - private static final ColorSettings.ColorProperty KEYWORD2_COLOR = - ColorSettings.define("[key]keyword2", "", new Color(0x78526C)); - - /** highight color for comments (dull green) */ - private static final ColorSettings.ColorProperty COMMENT_COLOR = - ColorSettings.define("[key]comment", "", new Color(0x3f7f5f)); - - /** highight color for literals (dark blue) */ - private static final ColorSettings.ColorProperty LITERAL_COLOR = - ColorSettings.define("[key]literal", "", new Color(0x2A75B1)); - - /** highight color for Modalities (dark yellow) */ - private static final ColorSettings.ColorProperty MODALITY_COLOR = - ColorSettings.define("[key]modality", "", new Color(0xC67C13)); - - /** default style */ - private static final SimpleAttributeSet normalStyle = new SimpleAttributeSet(); - - /** the style of keywords */ - private static final SimpleAttributeSet commentStyle = new SimpleAttributeSet(); - - /** the style of keywords */ - private static final SimpleAttributeSet keywordStyle = new SimpleAttributeSet(); - - /** the style of secondary keywords */ - private static final SimpleAttributeSet keyword2Style = new SimpleAttributeSet(); - - /** the style of literals */ - private static final SimpleAttributeSet literalStyle = new SimpleAttributeSet(); - - /** the style of comments and line comments */ - private static final SimpleAttributeSet modalityStyle = new SimpleAttributeSet(); - - /** the token identifiers for keywords */ - private static final BitSet KEYWORDS = new BitSet(); - - /** the token identifiers for secondary keywords */ - private static final BitSet KEYWORDS2 = new BitSet(); - - /** the token identifiers for literals */ - private static final BitSet LITERALS = new BitSet(); - - /** the token identifiers for comments */ - private static final BitSet COMMENTS = new BitSet(); - - /** the token identifiers for modalities */ - private static final BitSet MODALITIES = new BitSet(); - - static { - // set the styles - // StyleConstants.setBold(keywordStyle, true); - StyleConstants.setForeground(keywordStyle, KEYWORD_COLOR.get()); - StyleConstants.setForeground(keyword2Style, KEYWORD2_COLOR.get()); - StyleConstants.setForeground(commentStyle, COMMENT_COLOR.get()); - StyleConstants.setForeground(literalStyle, LITERAL_COLOR.get()); - StyleConstants.setForeground(modalityStyle, MODALITY_COLOR.get()); - - // the following can probably be refined - addAll(KEYWORDS, SORTS, GENERIC, PROXY, EXTENDS, ONEOF, ABSTRACT, SCHEMAVARIABLES, - SCHEMAVAR, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, - GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED, SAME_OBSERVER, VARCOND, - FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, INCLUDELDTS, CLASSPATH, - BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, - PROFILE, SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, - CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, HELPTEXT, REPLACEWITH, ADDRULES, - ADDPROGVARS, HEURISTICS, FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, FUNCTIONS, - DATATYPES, TRANSFORMERS, UNIQUE, FREE, RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, - PROOFOBLIGATION, PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, IN_TYPE, - IS_ABSTRACT_OR_INTERFACE, CONTAINERTYPE); - addAll(KEYWORDS2, MODALOPERATOR, PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, - SKOLEMTERM, SKOLEMFORMULA, TERMLABEL, VARIABLES, VARIABLE, APPLY_UPDATE_ON_RIGID, - DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, DROP_EFFECTLESS_STORES, - SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, FREELABELIN, HASSORT, FIELDTYPE, FINAL, - ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, - ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, ISTHISREFERENCE, - DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, ISMODELFIELD, - ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, - NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, - SAME, STATIC, STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, - INSTANTIATE_GENERIC); - addAll(LITERALS, STRING_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, DOUBLE_LITERAL, - REAL_LITERAL, TRUE, FALSE); - addAll(COMMENTS, DOC_COMMENT, ML_COMMENT, SL_COMMENT); - addAll(MODALITIES, MODALITY); - } - - private static void addAll(BitSet bitSet, int... values) { - for (int value : values) { - bitSet.set(value); - } - } - - private SimpleAttributeSet getAttributes(int type) { - if (KEYWORDS.get(type)) { - return keywordStyle; - } else if (KEYWORDS2.get(type)) { - return keyword2Style; - } else if (LITERALS.get(type)) { - return literalStyle; - } else if (COMMENTS.get(type)) { - return commentStyle; - } else if (MODALITIES.get(type)) { - return modalityStyle; - } else { - return normalStyle; - } - } - - @Override - public List applyTo(String text) { - JavaKeYLexer keYLexer = new JavaKeYLexer(CharStreams.fromString(text)); - List result = new ArrayList<>(); - var t = keYLexer.nextToken(); - while (t.getType() != -1) { - result.add(new SourceHighlightDocument.Token(t.getText().length(), - getAttributes(t.getType()))); - t = keYLexer.nextToken(); - } - return result; - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java index 09f93a21418..39a592d420a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java @@ -4,12 +4,17 @@ package de.uka.ilkd.key.gui.utilities; import java.awt.*; +import java.util.ArrayList; +import java.util.BitSet; +import java.util.List; import java.util.regex.Matcher; import java.util.regex.Pattern; import javax.swing.*; import javax.swing.text.*; import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.gui.sourceview.SourceHighlightDocument; +import de.uka.ilkd.key.nparser.JavaKeYLexer; import de.uka.ilkd.key.nparser.ParsingFacade; import org.antlr.v4.runtime.CharStreams; @@ -27,9 +32,16 @@ */ @NullMarked public abstract class LexerHighlighter { + private final StyleContext styleContext = new StyleContext(); + + /// Get the style regarding the `tokenType` of the {@link Token} protected abstract @Nullable AttributeSet getStyle(int tokenType); - private final StyleContext styleContext = new StyleContext(); + /// Length of the Markdown language prefix in code blocks. + protected abstract int getPatternPrefixLength(); + + /// The regular expression to find code blocks + protected abstract Pattern getMarkdownPattern(); protected AttributeSet define(Color fgColor, boolean bold, boolean italic) { AttributeSet aset = @@ -61,8 +73,6 @@ public final void highlightPaneMarkdown(JTextPane contentPane) { contentPane.repaint(); } - protected abstract int getPatternPrefixLength(); - public final void highlightPaneAll(JTextPane contentPane, int startIdx, int stopIdx) { String text = contentPane.getText(); @@ -87,7 +97,6 @@ public final void highlightPaneAll(JTextPane contentPane) { highlightPaneAll(contentPane, 0, -1); } - private void highlightToken(StyledDocument sd, int startIdx, Token tok) { var attribute = getStyle(tok.getType()); if (attribute != null) { @@ -97,104 +106,198 @@ private void highlightToken(StyledDocument sd, int startIdx, Token tok) { } } - protected abstract Pattern getMarkdownPattern(); + public SourceHighlightDocument.EditorLexer getEditorLexer() { + return text -> { + JavaKeYLexer keYLexer = new JavaKeYLexer(CharStreams.fromString(text)); + List result = new ArrayList<>(); + var t = keYLexer.nextToken(); + while (t.getType() != -1) { + result.add(new SourceHighlightDocument.Token(t.getText().length(), + getStyle(t.getType()))); + t = keYLexer.nextToken(); + } + return result; + }; + } public static class KeYLexerHighlighter extends LexerHighlighter { - public static final ColorSettings.ColorProperty COLOR_KEYWORD = - ColorSettings.define("infotree.syntax.keyword", "", Color.BLUE, Color.ORANGE); + + /** + * highlight color for KeY keywords (dark red/violet) + */ + private static final ColorSettings.ColorProperty COLOR_KEYWORD = + ColorSettings.define("syntax.key.keyword", "highlight color for KeY keywords ", + new Color(0x7f0055)); + + /** + * highlight color for secondary KeY keywords (light red/violet) + */ + private static final ColorSettings.ColorProperty COLOR_KEYWORD2 = + ColorSettings.define("syntax.key.keyword2", + "highlight color for secondary KeY keywords", new Color(0x78526C)); + + /** + * highlight color for comments (dull green) + */ + private static final ColorSettings.ColorProperty COLOR_COMMENT = + ColorSettings.define("syntax.key.comment", "highlight color for comments", + new Color(0xafafaf)); + + private static final ColorSettings.ColorProperty COLOR_COMMENT_DOC = + ColorSettings.define("syntax.key.comment", "highlight color for documentation comments", + new Color(0x3f7f5f)); + + /** + * highlight color for literals (dark blue) + */ + private static final ColorSettings.ColorProperty COLOR_LITERALS = + ColorSettings.define("syntax.key.literal", "highlight color for literals", + new Color(0x2A75B1)); + + /** + * highlight color for Modalities (dark yellow) + */ + private static final ColorSettings.ColorProperty COLOR_MODALITY = + ColorSettings.define("syntax.key.modality", "highlight color for Modalities", + new Color(0xC67C13)); public static final ColorSettings.ColorProperty COLOR_IDENTIFIER = ColorSettings.define("infotree.syntax.identifier", "", Color.BLACK, Color.WHITE); - public static final ColorSettings.ColorProperty COLOR_COMMENT = - ColorSettings.define("infotree.syntax.comment", "", Color.GREEN, Color.GREEN); - public static final ColorSettings.ColorProperty COLOR_OPERATORS = ColorSettings.define("infotree.syntax.operators", "", Color.BLACK, Color.ORANGE); public static final ColorSettings.ColorProperty COLOR_ERROR = ColorSettings.define("infotree.syntax.error", "", Color.RED, Color.WHITE); - public static final ColorSettings.ColorProperty COLOR_LITERALS = - ColorSettings.define("infotree.syntax.literals", "", Color.GREEN, Color.GREEN); - - public static final ColorSettings.ColorProperty COLOR_MODALITY = - ColorSettings.define("infotree.syntax.modality", "", Color.PINK, Color.PINK); - private final AttributeSet STYLE_OPERATORS = define(COLOR_OPERATORS.get(), false, false); private final AttributeSet STYLE_ERROR = define(COLOR_ERROR.get(), false, false); private final AttributeSet STYLE_LITERALS = define(COLOR_LITERALS.get(), false, true); private final AttributeSet STYLE_KEYWORDS = define(COLOR_KEYWORD.get(), true, false); + private final AttributeSet STYLE_KEYWORDS2 = define(COLOR_KEYWORD2.get(), false, false); private final AttributeSet STYLE_IDENTIFIER = define(COLOR_IDENTIFIER.get(), true, false); private final AttributeSet STYLE_COMMENT = define(COLOR_COMMENT.get(), false, true); + private final AttributeSet STYLE_COMMENT2 = define(COLOR_COMMENT_DOC.get(), false, true); private final AttributeSet STYLE_MODALITY = define(COLOR_MODALITY.get(), false, true); private final AttributeSet STYLE_DEFAULT = define(COLOR_IDENTIFIER.get(), false, false); + private final BitSet KEYWORDS = new BitSet(); + private final BitSet KEYWORDS2 = new BitSet(); + private final BitSet LITERALS = new BitSet(); + private final BitSet COMMENTS = new BitSet(); + private final BitSet COMMENTS2 = new BitSet(); + private final BitSet MODALITIES = new BitSet(); + private final BitSet IDENTIFIERS = new BitSet(); + private final BitSet ERROR = new BitSet(); + private final BitSet OPERATORS = new BitSet(); + + public KeYLexerHighlighter() { + // the following can probably be refined + addAll(KEYWORDS, SORTS, GENERIC, PROXY, EXTENDS, ONEOF, ABSTRACT, SCHEMAVARIABLES, + SCHEMAVAR, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, + HAS_INVARIANT, + GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED, SAME_OBSERVER, VARCOND, + FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, INCLUDELDTS, CLASSPATH, + BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, + PROFILE, SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, + CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, HELPTEXT, REPLACEWITH, + ADDRULES, + ADDPROGVARS, HEURISTICS, FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, FUNCTIONS, + DATATYPES, TRANSFORMERS, UNIQUE, FREE, RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, + PROOFOBLIGATION, PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, IN_TYPE, + IS_ABSTRACT_OR_INTERFACE, CONTAINERTYPE, + TERMLABEL, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, + HAS_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, + IS_LABELED, SAME_OBSERVER, VARCOND, APPLY_UPDATE_ON_RIGID, + DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, + DROP_EFFECTLESS_STORES, SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, + FREELABELIN, HASSORT, FIELDTYPE, FINAL, ELEMSORT, HASLABEL, + HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, + ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, + ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, + ISSTATICFIELD, ISMODELFIELD, ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, + NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, + NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, SAME, STATIC, + STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, INSTANTIATE_GENERIC, + FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, + INCLUDELDTS, CLASSPATH, BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, + WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, PROFILE, + SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, + CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, + HELPTEXT, REPLACEWITH, ADDRULES, ADDPROGVARS, HEURISTICS, + FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, + FUNCTIONS, DATATYPES, TRANSFORMERS, UNIQUE, FREE, + RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, PROOFOBLIGATION, + PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, + IN_TYPE, IS_ABSTRACT_OR_INTERFACE, IS_FINAL, CONTAINERTYPE, + SCHEMAVAR, FORMULA, MODALITYD, MODALITYB, + MODALITYBB, MODAILITYGENERIC1, MODAILITYGENERIC2, MODAILITYGENERIC3, + MODAILITYGENERIC4, MODAILITYGENERIC5, MODAILITYGENERIC6, MODAILITYGENERIC7, + MODALITYD_END, MODALITYD_STRING, MODALITYD_CHAR, MODALITYG_END, + MODALITYB_END, MODALITYBB_END, PROGRAM); + addAll(KEYWORDS2, MODALOPERATOR, PROGRAM, FORMULA, TERM, UPDATE, VARIABLES, VARIABLE, + SKOLEMTERM, SKOLEMFORMULA, TERMLABEL, VARIABLES, VARIABLE, APPLY_UPDATE_ON_RIGID, + DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, + DROP_EFFECTLESS_STORES, + SIMPLIFY_IF_THEN_ELSE_UPDATE, ISENUMCONST, FREELABELIN, HASSORT, FIELDTYPE, FINAL, + ELEMSORT, HASLABEL, HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, + ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, ISTHISREFERENCE, + DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, ISSTATICFIELD, ISMODELFIELD, + ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, + NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, + SAME, STATIC, STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, + INSTANTIATE_GENERIC); + addAll(OPERATORS, AT, PARALLEL, OR, AND, NOT, IMP, + EQUALS, NOT_EQUALS, SEQARROW, EXP, TILDE, PERCENT, + STAR, MINUS, PLUS, GREATER, GREATEREQUAL, + LESS, LESSEQUAL, LGUILLEMETS, RGUILLEMETS, EQV, + UTF_PRECEDES, UTF_IN, UTF_EMPTY, UTF_UNION, UTF_INTERSECT, + UTF_SUBSET_EQ, UTF_SUBSEQ, UTF_SETMINUS, SEMI, SLASH, + COLON, DOUBLECOLON, ASSIGN, DOT, DOTRANGE, COMMA, + LPAREN, RPAREN, LBRACE, RBRACE, LBRACKET, RBRACKET, + EMPTYBRACKETS); + addAll(ERROR, ERROR_UKNOWN_ESCAPE, ERROR_CHAR); + addAll(IDENTIFIERS, IDENT); + addAll(LITERALS, + CHAR_LITERAL, QUOTED_STRING_LITERAL, TRUE, FALSE, + STRING_LITERAL, BIN_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, + DOUBLE_LITERAL, REAL_LITERAL); + addAll(COMMENTS2, DOC_COMMENT); + addAll(COMMENTS, ML_COMMENT, SL_COMMENT, COMMENT_END); + addAll(MODALITIES, MODALITY); + } + + private static void addAll(BitSet bitSet, int... values) { + for (int value : values) { + bitSet.set(value); + } + } + @Override - protected @Nullable AttributeSet getStyle(int tokType) { - return switch (tokType) { - case TERMLABEL, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, - HAS_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, - IS_LABELED, SAME_OBSERVER, VARCOND, APPLY_UPDATE_ON_RIGID, - DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, - DROP_EFFECTLESS_STORES, SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, - FREELABELIN, HASSORT, FIELDTYPE, FINAL, ELEMSORT, HASLABEL, - HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, - ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, - ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, - ISSTATICFIELD, ISMODELFIELD, ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, - NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, - NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, SAME, STATIC, - STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, INSTANTIATE_GENERIC, - FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, - INCLUDELDTS, CLASSPATH, BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, - WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, PROFILE, - SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, - CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, - HELPTEXT, REPLACEWITH, ADDRULES, ADDPROGVARS, HEURISTICS, - FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, - FUNCTIONS, DATATYPES, TRANSFORMERS, UNIQUE, FREE, - RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, PROOFOBLIGATION, - PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, - IN_TYPE, IS_ABSTRACT_OR_INTERFACE, IS_FINAL, CONTAINERTYPE, - SCHEMAVAR, FORMULA, - COMMENT_END, DOC_COMMENT, ML_COMMENT, MODALITYD, MODALITYB, - MODALITYBB, MODAILITYGENERIC1, MODAILITYGENERIC2, MODAILITYGENERIC3, - MODAILITYGENERIC4, MODAILITYGENERIC5, MODAILITYGENERIC6, MODAILITYGENERIC7, - MODALITYD_END, MODALITYD_STRING, MODALITYD_CHAR, MODALITYG_END, - MODALITYB_END, MODALITYBB_END, MODALOPERATOR, PROGRAM -> - STYLE_KEYWORDS; - - case MODALITY -> STYLE_MODALITY; - - case AT, PARALLEL, OR, AND, NOT, IMP, - EQUALS, NOT_EQUALS, SEQARROW, EXP, TILDE, PERCENT, - STAR, MINUS, PLUS, GREATER, GREATEREQUAL, - LESS, LESSEQUAL, LGUILLEMETS, RGUILLEMETS, EQV, - UTF_PRECEDES, UTF_IN, UTF_EMPTY, UTF_UNION, UTF_INTERSECT, - UTF_SUBSET_EQ, UTF_SUBSEQ, UTF_SETMINUS, SEMI, SLASH, - COLON, DOUBLECOLON, ASSIGN, DOT, DOTRANGE, COMMA, - LPAREN, RPAREN, LBRACE, RBRACE, LBRACKET, RBRACKET, - EMPTYBRACKETS -> - STYLE_OPERATORS; - case ERROR_UKNOWN_ESCAPE, ERROR_CHAR -> STYLE_ERROR; - case IDENT -> STYLE_IDENTIFIER; - // 'COMMENT' is a lexer *mode*, not a token type; mode and token ids share one int - // space, so as a case label it aliases whatever token has the same id -- a - // duplicate - // case label once the modality lexer modes renumbered things (#3867). It was a dead - // no-op anyway: single-line comments are SL_COMMENT (here); a whole '/* ... */' / - // '/*! ... */' is emitted as COMMENT_END / DOC_COMMENT (currently grouped with the - // keywords above; ML_COMMENT is a 'more' rule and never a token). - case SL_COMMENT -> STYLE_COMMENT; - case CHAR_LITERAL, QUOTED_STRING_LITERAL, TRUE, FALSE, - STRING_LITERAL, BIN_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, - DOUBLE_LITERAL, REAL_LITERAL -> - STYLE_LITERALS; - default -> STYLE_DEFAULT; - }; + protected @Nullable AttributeSet getStyle(int type) { + if (KEYWORDS.get(type)) { + return STYLE_KEYWORDS; + } else if (KEYWORDS2.get(type)) { + return STYLE_KEYWORDS2; + } else if (LITERALS.get(type)) { + return STYLE_LITERALS; + } else if (COMMENTS2.get(type)) { + return STYLE_COMMENT2; + } else if (COMMENTS.get(type)) { + return STYLE_COMMENT; + } else if (ERROR.get(type)) { + return STYLE_ERROR; + } else if (IDENTIFIERS.get(type)) { + return STYLE_IDENTIFIER; + } else if (OPERATORS.get(type)) { + return STYLE_OPERATORS; + } else if (MODALITIES.get(type)) { + return STYLE_MODALITY; + } else { + return STYLE_DEFAULT; + } } @Override