diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json deleted file mode 100644 index ea948f6b773..00000000000 --- a/.devcontainer/devcontainer.json +++ /dev/null @@ -1,29 +0,0 @@ -// For format details, see https://aka.ms/devcontainer.json. For config options, see the -// README at: https://github.com/devcontainers/templates/tree/main/src/java -{ - "name": "Java", - // Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile - "image": "mcr.microsoft.com/devcontainers/java:0-17", - "features": { - "ghcr.io/devcontainers/features/java:1": { - "version": "none", - "installMaven": "false", - "installGradle": "true" - } - }, - "customizations": { - "vscode": { - "extensions": [ - "vscjava.vscode-gradle" - ] - } - }, - // Use 'forwardPorts' to make a list of ports inside the container available locally. - // "forwardPorts": [], - // Use 'postCreateCommand' to run commands after the container is created. - "postCreateCommand": "java -version" - // Configure tool-specific properties. - // "customizations": {}, - // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root. - // "remoteUser": "root" -} \ No newline at end of file diff --git a/key.core.example/src/main/java/org/key_project/Main.java b/key.core.example/src/main/java/org/key_project/Main.java index a6fc3b74a52..7c498d9dbd1 100644 --- a/key.core.example/src/main/java/org/key_project/Main.java +++ b/key.core.example/src/main/java/org/key_project/Main.java @@ -1,10 +1,7 @@ package org.key_project; import java.io.File; -import java.util.HashMap; -import java.util.LinkedList; -import java.util.List; -import java.util.Set; +import java.util.*; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.java.abstraction.KeYJavaType; @@ -69,8 +66,8 @@ private static KeYEnvironment setupEnvironment(File location) throws ProblemL } // Set Taclet options ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - HashMap oldSettings = choiceSettings.getDefaultChoices(); - HashMap newSettings = new HashMap<>(oldSettings); + Map oldSettings = choiceSettings.getDefaultChoices(); + Map newSettings = new HashMap<>(oldSettings); newSettings.putAll(MiscTools.getDefaultTacletOptions()); choiceSettings.setDefaultChoices(newSettings); // Load source code diff --git a/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java b/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java index 271cee95224..c889e717df5 100644 --- a/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java +++ b/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java @@ -1,9 +1,9 @@ package de.uka.ilkd.key.proof_references.testcase; import java.io.File; -import java.util.HashMap; import java.util.Iterator; import java.util.LinkedHashSet; +import java.util.Map; import java.util.function.Predicate; import de.uka.ilkd.key.control.KeYEnvironment; @@ -63,7 +63,8 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir, IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences) throws Exception { doReferenceFunctionTest(baseDir, javaPathInBaseDir, containerTypeName, targetName, - useContracts, analyst, null, expectedReferences); + useContracts, analyst, + null, expectedReferences); } /** @@ -306,7 +307,7 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir, assertNotNull(tester); KeYEnvironment environment = null; Proof proof = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean usePrettyPrinting = ProofIndependentSettings.isUsePrettyPrinting(); try { // Disable pretty printing to make tests more robust against different term @@ -379,7 +380,7 @@ protected void doProofMethodTest(File baseDir, String javaPathInBaseDir, assertNotNull(tester); KeYEnvironment environment = null; Proof proof = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean usePrettyPrinting = ProofIndependentSettings.isUsePrettyPrinting(); try { // Disable pretty printing to make tests more robust against different term diff --git a/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java index 59fccf80d10..94dceb21784 100644 --- a/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java +++ b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java @@ -3,6 +3,7 @@ import java.io.File; import java.util.HashMap; import java.util.List; +import java.util.Map; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -61,8 +62,8 @@ public static void main(String[] args) { } // Set Taclet options ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - HashMap oldSettings = choiceSettings.getDefaultChoices(); - HashMap newSettings = new HashMap<>(oldSettings); + Map oldSettings = choiceSettings.getDefaultChoices(); + Map newSettings = new HashMap<>(oldSettings); newSettings.putAll(MiscTools.getDefaultTacletOptions()); newSettings.put("methodExpansion", "methodExpansion:noRestriction"); choiceSettings.setDefaultChoices(newSettings); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index 0757d23f812..c0e5a81ee2e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -2782,9 +2782,9 @@ public static String getChoiceSetting(String key) { * @param value The new choice value to set. */ public static void setChoiceSetting(String key, String value) { - HashMap settings = + var settings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - HashMap clone = new LinkedHashMap<>(settings); + var clone = new LinkedHashMap<>(settings); clone.put(key, value); ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone); } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java index 2d5237f2864..f1910afd1ff 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java @@ -2012,7 +2012,7 @@ protected SymbolicExecutionEnvironment doSETTest(Fi boolean variablesAreOnlyComputedFromUpdates, boolean simplifyConditions) throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Make sure that parameter are valid. @@ -2105,7 +2105,7 @@ protected SymbolicExecutionEnvironment doSETTest(Fi boolean variablesAreOnlyComputedFromUpdates, boolean truthValueEvaluationEnabled, boolean simplifyConditions) throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; try { // Make sure that parameter are valid. assertNotNull(javaPathInBaseDir); @@ -2195,13 +2195,16 @@ private void internalDoSETTest(File oracleFile, * @throws ProblemLoaderException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public static HashMap setDefaultTacletOptions(File baseDir, + public static Map setDefaultTacletOptions(File baseDir, String javaPathInBaseDir, String baseContractName) throws ProblemLoaderException, ProofInputException { if (!SymbolicExecutionUtil.isChoiceSettingInitialised()) { SymbolicExecutionEnvironment env = createSymbolicExecutionEnvironment(testCaseDirectory, javaPathInBaseDir, - baseContractName, false, false, false, false, false, false, false, false, false, + baseContractName, + false, false, false, + false, false, false, + false, false, false, false, false); env.dispose(); } @@ -2219,14 +2222,18 @@ public static HashMap setDefaultTacletOptions(File baseDir, * @throws ProblemLoaderException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public static HashMap setDefaultTacletOptions(File baseDir, - String javaPathInBaseDir, String containerTypeName, String methodFullName) + public static Map setDefaultTacletOptions(File baseDir, + String javaPathInBaseDir, + String containerTypeName, + String methodFullName) throws ProblemLoaderException, ProofInputException { if (!SymbolicExecutionUtil.isChoiceSettingInitialised()) { SymbolicExecutionEnvironment env = createSymbolicExecutionEnvironment(baseDir, javaPathInBaseDir, containerTypeName, - methodFullName, null, false, false, false, false, false, false, false, false, - false, false); + methodFullName, + null, false, false, false, + false, false, false, false, + false, false, false); env.dispose(); } return setDefaultTacletOptions(); @@ -2242,7 +2249,7 @@ public static HashMap setDefaultTacletOptions(File baseDir, * @throws ProblemLoaderException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public static HashMap setDefaultTacletOptionsForTarget(File javaFile, + public static Map setDefaultTacletOptionsForTarget(File javaFile, String containerTypeName, final String targetName) throws ProblemLoaderException, ProofInputException { return HelperClassForTests.setDefaultTacletOptionsForTarget(javaFile, containerTypeName, @@ -2254,8 +2261,8 @@ public static HashMap setDefaultTacletOptionsForTarget(File java * * @return The original settings which are overwritten. */ - public static HashMap setDefaultTacletOptions() { - HashMap original = HelperClassForTests.setDefaultTacletOptions(); + public static Map setDefaultTacletOptions() { + Map original = HelperClassForTests.setDefaultTacletOptions(); ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); ImmutableSet cs = DefaultImmutableSet.nil(); cs = cs.add(new Choice("noRestriction", "methodExpansion")); @@ -2268,7 +2275,7 @@ public static HashMap setDefaultTacletOptions() { * * @param options The taclet options to restore. */ - public static void restoreTacletOptions(HashMap options) { + public static void restoreTacletOptions(Map options) { HelperClassForTests.restoreTacletOptions(options); } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java index 8aede3496cb..1e18797423b 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java @@ -1,8 +1,8 @@ package de.uka.ilkd.key.symbolic_execution.testcase; import java.io.File; -import java.util.HashMap; import java.util.Iterator; +import java.util.Map; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -20,6 +20,7 @@ import static org.junit.jupiter.api.Assertions.*; + /** * Tests for {@link SymbolicExecutionTreeBuilder}, * {@link ExecutedSymbolicExecutionTreeNodesStopCondition} and {@link SymbolicExecutionGoalChooser}. @@ -536,7 +537,7 @@ public void testComplexPruning() throws Exception { @Test public void testSymbolicExecutionCompletionsTest() throws Exception { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { String javaPathInBaseDir = diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java index 263d1c86527..cd62a077e03 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java @@ -3,9 +3,9 @@ import java.io.File; import java.io.IOException; import java.util.ArrayList; -import java.util.HashMap; import java.util.Iterator; import java.util.List; +import java.util.Map; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.symbolic_execution.SymbolicLayoutExtractor; @@ -24,6 +24,7 @@ import static org.junit.jupiter.api.Assertions.*; + /** * Tests {@link SymbolicLayoutExtractor}. * @@ -529,7 +530,7 @@ protected void doTest(String javaPathInkeyRepDirectory, String containerTypeName String precondition, int numberOfReturnNodeInMostLeftBranch, int expectedNumberOfLayouts, boolean useOperationContracts, boolean onReturnStatementNode) throws Exception { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; SymbolicExecutionEnvironment env = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java index 62a8ea11c3b..4318ba8a65c 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.po; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -40,7 +40,7 @@ public void testDoubleValue() throws Exception { protected void doTest(String javaPathInkeyRepDirectory, String baseContractName, String oraclePathInBaseDirFile, String expectedTryContent) throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; SymbolicExecutionEnvironment env = null; try { // Make sure that the correct taclet options are defined. diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java index 8585fc26438..a8de6e28d3a 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.po; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -108,7 +108,7 @@ protected void doTest(String javaPathInkeyRepDirectory, String containerTypeName String methodFullName, String oraclePathInBaseDirFile, String precondition, String expectedTryContent) throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; SymbolicExecutionEnvironment env = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java index 30e58ed5f94..8e234929312 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -29,7 +29,7 @@ public class TestExceptionBreakpointStopConditionCaughtOrUncaught public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java index 482dde95a61..b87db5314c6 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -23,7 +23,7 @@ public class TestExceptionBreakpointStopConditionWithHitCount @Test public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); SymbolicExecutionEnvironment env = null; try { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java index 24393189ca5..9e2a86b3100 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -23,7 +23,7 @@ public class TestExceptionBreakpointStopConditionWithSubclasses @Test // weigl not prev. activated public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); SymbolicExecutionEnvironment env = null; try { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java index 8fb9ef55849..9f9cf4fc787 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -22,7 +22,7 @@ public class TestJavaWatchpointStopConditionWithHitCount extends AbstractSymboli public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java index f7bb685eeff..34c80d54223 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -24,7 +24,7 @@ public class TestKeYWatchpointGlobalVariablesOnSatisfiable public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnTrueWithHitCount.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnTrueWithHitCount.java index 478e7b4553b..104fb8a3fe2 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnTrueWithHitCount.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnTrueWithHitCount.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -24,7 +24,7 @@ public class TestKeYWatchpointGlobalVariablesOnTrueWithHitCount public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointMethodsOnSatisfiable.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointMethodsOnSatisfiable.java index 0542e7c1e2a..cf3d0c2d47c 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointMethodsOnSatisfiable.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointMethodsOnSatisfiable.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -23,7 +23,7 @@ public class TestKeYWatchpointMethodsOnSatisfiable extends AbstractSymbolicExecu public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithConditions.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithConditions.java index b8ddd08a4fa..96bc3f44b34 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithConditions.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithConditions.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -25,7 +25,7 @@ public void testBreakpointStopCondition() throws ProofInputException, IOExceptio SymbolicExecutionEnvironment envMain = null; SymbolicExecutionEnvironment envSomethingMain = null; SymbolicExecutionEnvironment envSomethingLocalMain = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithHitCount.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithHitCount.java index d872416615d..25dda6743ae 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithHitCount.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithHitCount.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -28,7 +28,7 @@ public class TestLineBreakpointStopConditionSimpleWithHitCount @Test // weigl not prev. activated public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); SymbolicExecutionEnvironment env = null; try { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithLoopInvariant.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithLoopInvariant.java index 1a6e4eab77f..4c1b516e4a5 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithLoopInvariant.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithLoopInvariant.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -26,7 +26,7 @@ public void testBreakpointStopCondition() throws ProofInputException, IOExceptio SymbolicExecutionEnvironment envMain = null; SymbolicExecutionEnvironment envSomethingMain = null; SymbolicExecutionEnvironment envSomethingLocalMain = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithConditions.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithConditions.java index a9964614a0c..256c864ece1 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithConditions.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithConditions.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -24,7 +24,7 @@ public void testBreakpointStopCondition() throws ProofInputException, IOExceptio SymbolicExecutionEnvironment envMain = null; SymbolicExecutionEnvironment envSomethingMain = null; SymbolicExecutionEnvironment envSomethingLocalMain = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithHitCount.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithHitCount.java index 9b39a882126..c69e16bd6fe 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithHitCount.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithHitCount.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -22,7 +22,7 @@ public class TestMethodBreakpointWithHitCount extends AbstractSymbolicExecutionT public void testBreakpointStopCondition() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { SymbolicExecutionEnvironment env = null; - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); try { // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepOverSymbolicExecutionTreeNodesStopCondition.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepOverSymbolicExecutionTreeNodesStopCondition.java index 9e7643bdb70..377a3f4ac61 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepOverSymbolicExecutionTreeNodesStopCondition.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepOverSymbolicExecutionTreeNodesStopCondition.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -33,7 +33,7 @@ public class TestStepOverSymbolicExecutionTreeNodesStopCondition @Test // weigl not prev. activated public void testStepOverOnTwoBranches() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; SymbolicExecutionEnvironment env = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepReturnSymbolicExecutionTreeNodesStopCondition.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepReturnSymbolicExecutionTreeNodesStopCondition.java index 6fd1e912565..afdb0b49900 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepReturnSymbolicExecutionTreeNodesStopCondition.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepReturnSymbolicExecutionTreeNodesStopCondition.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.strategy; import java.io.IOException; -import java.util.HashMap; +import java.util.Map; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -31,7 +31,7 @@ public class TestStepReturnSymbolicExecutionTreeNodesStopCondition @Test // weigl was not prev. activated public void testStepReturn() throws ProofInputException, IOException, ParserConfigurationException, SAXException, ProblemLoaderException { - HashMap originalTacletOptions = null; + Map originalTacletOptions = null; SymbolicExecutionEnvironment env = null; boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null); // Define test settings diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index 448dc69321d..f7531889b8a 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -1,7 +1,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.util; import java.io.File; -import java.util.HashMap; +import java.util.Map; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.java.Services; @@ -121,7 +121,7 @@ public void test2GetAndSetChoiceSetting() { // weigl: disable, no clue why the choice settings should be initialised // assertTrue(SymbolicExecutionUtil.isChoiceSettingInitialised()); // Store default choice settings - HashMap defaultSettings = + Map defaultSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); // weigl: disable, no clue why the choice settings should be initialised // assertFalse(defaultSettings.isEmpty()); @@ -142,7 +142,7 @@ public void test2GetAndSetChoiceSetting() { Assertions.assertEquals(newValue, SymbolicExecutionUtil .getChoiceSetting(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS)); // Make sure that all other settings are unchanged. - HashMap changedSettings = + Map changedSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); defaultSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue); Assertions.assertEquals(defaultSettings, changedSettings); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java index 22aa1f26214..014ed1541b9 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java @@ -1,14 +1,11 @@ package de.uka.ilkd.key.settings; import java.io.File; -import java.util.Collection; -import java.util.EventObject; -import java.util.LinkedHashSet; import java.util.Properties; import javax.annotation.Nonnull; import javax.annotation.Nullable; -public class TestGenerationSettings implements Settings, Cloneable { +public class TestGenerationSettings extends AbstractSettings { // region Default Values for option fields private static final boolean DEFAULT_APPLYSYMBOLICEX = false; private static final int DEFAULT_MAXUNWINDS = 3; @@ -40,7 +37,6 @@ public class TestGenerationSettings implements Settings, Cloneable { "[TestGenSettings]IncludePostCondition"; // endregion - private final Collection listeners; // Option fields private boolean applySymbolicExecution; private int maxUnwinds; @@ -56,7 +52,6 @@ public class TestGenerationSettings implements Settings, Cloneable { public TestGenerationSettings() { - listeners = new LinkedHashSet<>(); applySymbolicExecution = TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX; maxUnwinds = TestGenerationSettings.DEFAULT_MAXUNWINDS; outputPath = TestGenerationSettings.DEFAULT_OUTPUTPATH; @@ -71,8 +66,6 @@ public TestGenerationSettings() { } public TestGenerationSettings(TestGenerationSettings data) { - listeners = new LinkedHashSet<>(); - listeners.addAll(data.listeners); applySymbolicExecution = data.applySymbolicExecution; maxUnwinds = data.maxUnwinds; outputPath = data.outputPath; @@ -87,25 +80,16 @@ public TestGenerationSettings(TestGenerationSettings data) { } - @Override - public void addSettingsListener(SettingsListener l) { - listeners.add(l); - } - - @Override - public void removeSettingsListener(SettingsListener l) { - listeners.remove(l); - } - - // FIXME weigl: This method seems broken. I would expect: clone() = new TGS(this) + /** + * @deprecated weigl: This method seems broken. I would expect: clone() = new TGS(this) + */ + @Deprecated(forRemoval = true) public TestGenerationSettings clone(TestGenerationSettings data) { return new TestGenerationSettings(data); } - public void fireSettingsChanged() { - for (final SettingsListener aListenerList : listeners) { - aListenerList.settingsChanged(new EventObject(this)); - } + public TestGenerationSettings clone() { + return new TestGenerationSettings(this); } public boolean getApplySymbolicExecution() { @@ -113,7 +97,9 @@ public boolean getApplySymbolicExecution() { } public void setApplySymbolicExecution(boolean applySymbolicExecution) { + var old = this.applySymbolicExecution; this.applySymbolicExecution = applySymbolicExecution; + firePropertyChange(PROP_APPLY_SYMBOLIC_EXECUTION, old, this.applySymbolicExecution); } public int getMaximalUnwinds() { @@ -138,35 +124,39 @@ public boolean includePostCondition() { @Override public void readSettings(Properties props) { - applySymbolicExecution = - SettingsConverter.read(props, TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION, - TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX); - maxUnwinds = SettingsConverter.read(props, TestGenerationSettings.PROP_MAX_UWINDS, - TestGenerationSettings.DEFAULT_MAXUNWINDS); - outputPath = SettingsConverter.read(props, TestGenerationSettings.PROP_OUTPUT_PATH, - TestGenerationSettings.DEFAULT_OUTPUTPATH); - removeDuplicates = - SettingsConverter.read(props, TestGenerationSettings.PROP_REMOVE_DUPLICATES, - TestGenerationSettings.DEFAULT_REMOVEDUPLICATES); - useRFL = SettingsConverter.read(props, TestGenerationSettings.PROP_USE_RFL, - TestGenerationSettings.DEFAULT_USERFL); - useJunit = SettingsConverter.read(props, TestGenerationSettings.PROP_USE_JUNIT, - TestGenerationSettings.DEFAULT_USEJUNIT); - concurrentProcesses = - SettingsConverter.read(props, TestGenerationSettings.PROP_CONCURRENT_PROCESSES, - TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES); - invariantForAll = - SettingsConverter.read(props, TestGenerationSettings.PROP_INVARIANT_FOR_ALL, - TestGenerationSettings.DEFAULT_INVARIANTFORALL); - openjmlPath = SettingsConverter.read(props, TestGenerationSettings.PROP_OPENJML_PATH, - TestGenerationSettings.DEFAULT_OPENJMLPATH); - - objenesisPath = SettingsConverter.read(props, TestGenerationSettings.PROP_OBJENESIS_PATH, - TestGenerationSettings.DEFAULT_OBJENESISPATH); - - includePostCondition = - SettingsConverter.read(props, TestGenerationSettings.PROP_INCLUDE_POST_CONDITION, - TestGenerationSettings.DEFAULT_INCLUDEPOSTCONDITION); + setApplySymbolicExecution(SettingsConverter.read(props, + TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION, + TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX)); + setMaxUnwinds(SettingsConverter.read(props, + TestGenerationSettings.PROP_MAX_UWINDS, + TestGenerationSettings.DEFAULT_MAXUNWINDS)); + setOutputPath(SettingsConverter.read(props, + TestGenerationSettings.PROP_OUTPUT_PATH, + TestGenerationSettings.DEFAULT_OUTPUTPATH)); + setRemoveDuplicates(SettingsConverter.read(props, + TestGenerationSettings.PROP_REMOVE_DUPLICATES, + TestGenerationSettings.DEFAULT_REMOVEDUPLICATES)); + setRFL(SettingsConverter.read(props, + TestGenerationSettings.PROP_USE_RFL, + TestGenerationSettings.DEFAULT_USERFL)); + setUseJunit(SettingsConverter.read(props, + TestGenerationSettings.PROP_USE_JUNIT, + TestGenerationSettings.DEFAULT_USEJUNIT)); + setConcurrentProcesses(SettingsConverter.read(props, + TestGenerationSettings.PROP_CONCURRENT_PROCESSES, + TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES)); + setInvariantForAll(SettingsConverter.read(props, + TestGenerationSettings.PROP_INVARIANT_FOR_ALL, + TestGenerationSettings.DEFAULT_INVARIANTFORALL)); + setOpenjmlPath(SettingsConverter.read(props, + TestGenerationSettings.PROP_OPENJML_PATH, + TestGenerationSettings.DEFAULT_OPENJMLPATH)); + setObjenesisPath(SettingsConverter.read(props, + TestGenerationSettings.PROP_OBJENESIS_PATH, + TestGenerationSettings.DEFAULT_OBJENESISPATH)); + setIncludePostCondition(SettingsConverter.read(props, + TestGenerationSettings.PROP_INCLUDE_POST_CONDITION, + TestGenerationSettings.DEFAULT_INCLUDEPOSTCONDITION)); } public boolean removeDuplicates() { @@ -174,35 +164,56 @@ public boolean removeDuplicates() { } public void setConcurrentProcesses(int concurrentProcesses) { + var old = this.concurrentProcesses; this.concurrentProcesses = concurrentProcesses; + firePropertyChange(PROP_CONCURRENT_PROCESSES, old, this.concurrentProcesses); } public void setInvariantForAll(boolean invariantForAll) { + var old = this.invariantForAll; this.invariantForAll = invariantForAll; + firePropertyChange(PROP_INVARIANT_FOR_ALL, old, this.invariantForAll); } public void setMaxUnwinds(int maxUnwinds) { + var old = this.maxUnwinds; this.maxUnwinds = maxUnwinds; + firePropertyChange(PROP_MAX_UWINDS, old, this.maxUnwinds); } public void setOutputPath(String outputPath) { + var old = this.outputPath; this.outputPath = outputPath; + firePropertyChange(PROP_OUTPUT_PATH, old, this.outputPath); + } public void setRemoveDuplicates(boolean removeDuplicates) { + var old = this.removeDuplicates; this.removeDuplicates = removeDuplicates; + firePropertyChange(PROP_REMOVE_DUPLICATES, old, this.removeDuplicates); + } public void setIncludePostCondition(boolean includePostCondition) { + var old = this.includePostCondition; this.includePostCondition = includePostCondition; + firePropertyChange(PROP_INCLUDE_POST_CONDITION, old, this.includePostCondition); + } public void setRFL(boolean useRFL) { + var old = this.useRFL; this.useRFL = useRFL; + firePropertyChange(PROP_USE_RFL, old, this.useRFL); + } public void setUseJunit(boolean useJunit) { + var old = this.useJunit; this.useJunit = useJunit; + firePropertyChange(PROP_USE_JUNIT, old, this.useJunit); + } public String getObjenesisPath() { @@ -210,7 +221,10 @@ public String getObjenesisPath() { } public void setObjenesisPath(String objenesisPath) { + var old = this.objenesisPath; this.objenesisPath = objenesisPath; + firePropertyChange(PROP_OBJENESIS_PATH, old, this.objenesisPath); + } public String getOpenjmlPath() { @@ -218,7 +232,9 @@ public String getOpenjmlPath() { } public void setOpenjmlPath(String openjmlPath) { + var old = this.openjmlPath; this.openjmlPath = openjmlPath; + firePropertyChange(PROP_OPENJML_PATH, old, this.openjmlPath); } public boolean useRFL() { @@ -257,7 +273,8 @@ public void set(TestGenerationSettings settings) { } - private static @Nullable TestGenerationSettings instance; + @Nullable + private static TestGenerationSettings instance; public static @Nonnull TestGenerationSettings getInstance() { if (instance == null) { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java index 2ad2a03d21a..16608ce593c 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java @@ -156,7 +156,7 @@ public void generateTestCases(final StopRequest stopRequest, final TestGeneratio final ProofDependentSMTSettings pdSettings = proof.getSettings().getSMTSettings().clone(); final NewSMTTranslationSettings newSettings = new NewSMTTranslationSettings(proof.getSettings().getNewSMTSettings()); - pdSettings.invariantForall = settings.invariantForAll(); + pdSettings.setInvariantForall(settings.invariantForAll()); // invoke z3 for counterexamples final DefaultSMTSettings smtsettings = new DefaultSMTSettings(pdSettings, piSettings, newSettings, proof); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java index 438e2ae172a..a6b0c0013f4 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java @@ -82,7 +82,7 @@ private SolverLauncher prepareLauncher() { piSettings.setMaxConcurrentProcesses(settings.getNumberOfProcesses()); final ProofDependentSMTSettings pdSettings = ProofDependentSMTSettings.getDefaultSettingsData(); - pdSettings.invariantForall = settings.invariantForAll(); + pdSettings.setInvariantForall(settings.invariantForAll()); // invoke z3 for counterexamples final DefaultSMTSettings smtsettings = new DefaultSMTSettings(pdSettings, piSettings, new NewSMTTranslationSettings(), null); diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/SMTTestSettings.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/SMTTestSettings.java index a51f92b49be..5f60b894531 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/SMTTestSettings.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/SMTTestSettings.java @@ -79,13 +79,13 @@ public boolean useUninterpretedMultiplicationIfNecessary() { @Override public long getMaximumInteger() { - return ProofDependentSMTSettings.getDefaultSettingsData().maxInteger; + return ProofDependentSMTSettings.getDefaultSettingsData().getMaxInteger(); } @Override public long getMinimumInteger() { - return ProofDependentSMTSettings.getDefaultSettingsData().minInteger; + return ProofDependentSMTSettings.getDefaultSettingsData().getMinInteger(); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java index d349cd2b54c..39f0414eac1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java @@ -650,7 +650,7 @@ public ProblemReport analyze() { public void makeExplicit() { // abort if JML is disabled // if(!ProofSettings.DEFAULT_SETTINGS.getGeneralSettings().useJML()) { - if (!ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().useJML()) { + if (!ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().isUseJML()) { return; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 5221b784def..fe918208c36 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.proof; +import java.beans.PropertyChangeListener; import java.io.File; import java.io.IOException; import java.util.*; @@ -29,7 +30,6 @@ import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; @@ -110,7 +110,7 @@ public class Proof implements Named { private Strategy activeStrategy; - private SettingsListener settingsListener; + private PropertyChangeListener settingsListener; /** * Set to true if the proof has been abandoned and the dispose method has been called on this @@ -157,7 +157,7 @@ private Proof(Name name, InitConfig initConfig) { localMgt = new ProofCorrectnessMgt(this); - initConfig.getSettings().getStrategySettings().addSettingsListener(settingsListener); + initConfig.getSettings().getStrategySettings().addPropertyChangeListener(settingsListener); pis = ProofIndependentSettings.DEFAULT_INSTANCE; } @@ -261,7 +261,8 @@ public void dispose() { // contained in a static List } // remove setting listener from settings - initConfig.getSettings().getStrategySettings().removeSettingsListener(settingsListener); + initConfig.getSettings().getStrategySettings() + .removePropertyChangeListener(settingsListener); // set every reference (except the name) to null root = null; env = null; @@ -275,8 +276,6 @@ public void dispose() { keyVersionLog = null; activeStrategy = null; settingsListener = null; - ruleAppListenerList.clear(); - listenerList.clear(); disposed = true; userData = null; fireProofDisposed(new ProofDisposedEvent(this)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index 9d01707ee64..394edb3ad0c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -50,7 +50,7 @@ public class InitConfig { * maps categories to their default choice (both represented as Strings), which is used if no * other choice is specified in the problemfile */ - private HashMap category2DefaultChoice = new LinkedHashMap<>(); + private Map category2DefaultChoice; /** * maps taclets to their TacletBuilders. This information is needed when a taclet contains @@ -86,8 +86,8 @@ public class InitConfig { public InitConfig(Services services) { this.services = services; - category2DefaultChoice = - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); + category2DefaultChoice = new HashMap<>( + ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices()); } @@ -140,9 +140,8 @@ public void addCategory2DefaultChoices(@Nonnull Map init) { if (changed) { // FIXME weigl: I do not understand why the default choices are back progragated! // For me this is a design flaw. - @SuppressWarnings("unchecked") - HashMap clone = - (HashMap) category2DefaultChoice.clone(); + Map clone = + new HashMap<>(category2DefaultChoice); ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone); // invalidate active taclet cache activatedTacletCache = null; @@ -175,8 +174,7 @@ public void setActivatedChoices(ImmutableSet activatedChoices) { category2DefaultChoice = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - @SuppressWarnings("unchecked") - HashMap c2DC = (HashMap) category2DefaultChoice.clone(); + HashMap c2DC = new HashMap<>(category2DefaultChoice); for (final Choice c : activatedChoices) { c2DC.remove(c.category()); } @@ -189,7 +187,8 @@ public void setActivatedChoices(ImmutableSet activatedChoices) { } } this.activatedChoices = activatedChoices - .union(DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList)); + .union( + DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList)); // invalidate active taclet cache activatedTacletCache = null; @@ -426,7 +425,7 @@ public InitConfig copyWithServices(Services services) { ic.setSettings(new ProofSettings(settings)); } ic.setActivatedChoices(activatedChoices); - ic.category2DefaultChoice = ((HashMap) category2DefaultChoice.clone()); + ic.category2DefaultChoice = new HashMap<>(category2DefaultChoice); ic.setTaclet2Builder( (HashMap>) taclet2Builder.clone()); ic.taclets = taclets; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java index f6c5d4813c7..abd9430c718 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.proof.io; +import java.beans.PropertyChangeListener; import java.io.File; import de.uka.ilkd.key.proof.Proof; @@ -7,7 +8,6 @@ import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.settings.GeneralSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.util.KeYConstants; import org.key_project.util.java.IOUtil; @@ -15,6 +15,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; + /** * Saves intermediate proof artifacts during strategy execution. An {@link AutoSaver} instance saves * periodically and the final proof state if it is closed. The default save interval can be set @@ -28,8 +29,8 @@ public class AutoSaver implements ProverTaskListener { public static final Logger LOGGER = LoggerFactory.getLogger(AutoSaver.class); - private final static File TMP_DIR = IOUtil.getTempDirectory(); - private final static String PREFIX = TMP_DIR + File.separator + ".autosave."; + private static final File TMP_DIR = IOUtil.getTempDirectory(); + private static final String PREFIX = TMP_DIR + File.separator + ".autosave."; private Proof proof; private final int interval; @@ -40,11 +41,12 @@ public class AutoSaver implements ProverTaskListener { private static AutoSaver DEFAULT_INSTANCE = null; - public final static SettingsListener settingsListener = e -> { - assert e.getSource() instanceof GeneralSettings; - GeneralSettings settings = (GeneralSettings) e.getSource(); - setDefaultValues(settings.autoSavePeriod(), settings.autoSavePeriod() > 0); - }; + public static final PropertyChangeListener settingsListener = + e -> { + assert e.getSource() instanceof GeneralSettings; + GeneralSettings settings = (GeneralSettings) e.getSource(); + setDefaultValues(settings.autoSavePeriod(), settings.autoSavePeriod() > 0); + }; /** * Set default values. diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index 2a8eda6181e..ffe569431a7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -12,7 +12,7 @@ * * @author weigl */ -public abstract class AbstractPropertiesSettings implements Settings { +public abstract class AbstractPropertiesSettings extends AbstractSettings { private static final String SET_DELIMITER = ","; private static final Function parseInt = Integer::parseInt; private static final Function parseFloat = Float::parseFloat; @@ -30,11 +30,6 @@ public abstract class AbstractPropertiesSettings implements Settings { */ protected final List> propertyEntries = new LinkedList<>(); - /** - * Collection of listeners to notify when a setting changes its value. - */ - protected final List listenerList = new LinkedList<>(); - private static Set parseStringSet(String o) { Set set = new TreeSet<>(); for (String entry : o.split(SET_DELIMITER)) { @@ -78,7 +73,6 @@ public boolean isInitialized() { @Override public void readSettings(Properties props) { - assert props != null; propertyEntries.forEach(it -> { String value = props.getProperty(it.getKey()); if (value != null) { @@ -93,22 +87,6 @@ public void writeSettings(Properties props) { props.putAll(properties); } - @Override - public void addSettingsListener(SettingsListener l) { - listenerList.add(l); - } - - @Override - public void removeSettingsListener(SettingsListener l) { - listenerList.remove(l); - } - - protected void fireSettingsChange() { - for (SettingsListener listener : listenerList) { - listener.settingsChanged(new EventObject(this)); - } - } - protected PropertyEntry createDoubleProperty(String key, double defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseDouble); propertyEntries.add(pe); @@ -215,9 +193,7 @@ public void set(T value) { // only store non-null values if (value != null) { properties.setProperty(key, toString.apply(value)); - if (!value.equals(old)) { - fireSettingsChange(); - } + firePropertyChange(key, old, value); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractSettings.java new file mode 100644 index 00000000000..d4cb7bb383d --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractSettings.java @@ -0,0 +1,78 @@ +package de.uka.ilkd.key.settings; + +import java.beans.PropertyChangeEvent; +import java.beans.PropertyChangeListener; +import java.beans.PropertyChangeSupport; + +/** + * @author Alexander Weigl + * @version 1 (1/30/22) + */ +public abstract class AbstractSettings implements Settings { + protected final PropertyChangeSupport changeSupport = new PropertyChangeSupport(this); + + @Override + public void addPropertyChangeListener(PropertyChangeListener listener) { + changeSupport.addPropertyChangeListener(listener); + } + + @Override + public void removePropertyChangeListener(PropertyChangeListener listener) { + changeSupport.removePropertyChangeListener(listener); + } + + @Override + public PropertyChangeListener[] getPropertyChangeListeners() { + return changeSupport.getPropertyChangeListeners(); + } + + @Override + public void addPropertyChangeListener(String propertyName, PropertyChangeListener listener) { + changeSupport.addPropertyChangeListener(propertyName, listener); + } + + @Override + public void removePropertyChangeListener(String propertyName, PropertyChangeListener listener) { + changeSupport.removePropertyChangeListener(propertyName, listener); + } + + + protected PropertyChangeListener[] getPropertyChangeListeners(String propertyName) { + return changeSupport.getPropertyChangeListeners(propertyName); + } + + protected void firePropertyChange(String propertyName, Object oldValue, Object newValue) { + changeSupport.firePropertyChange(propertyName, oldValue, newValue); + } + + protected void firePropertyChange(String propertyName, int oldValue, int newValue) { + changeSupport.firePropertyChange(propertyName, oldValue, newValue); + } + + protected void firePropertyChange(String propertyName, boolean oldValue, boolean newValue) { + changeSupport.firePropertyChange(propertyName, oldValue, newValue); + } + + protected void firePropertyChange(PropertyChangeEvent event) { + changeSupport.firePropertyChange(event); + } + + protected void fireIndexedPropertyChange(String propertyName, int index, Object oldValue, + Object newValue) { + changeSupport.fireIndexedPropertyChange(propertyName, index, oldValue, newValue); + } + + protected void fireIndexedPropertyChange(String propertyName, int index, int oldValue, + int newValue) { + changeSupport.fireIndexedPropertyChange(propertyName, index, oldValue, newValue); + } + + protected void fireIndexedPropertyChange(String propertyName, int index, boolean oldValue, + boolean newValue) { + changeSupport.fireIndexedPropertyChange(propertyName, index, oldValue, newValue); + } + + protected boolean hasListeners(String propertyName) { + return changeSupport.hasListeners(propertyName); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index d0f5194dd21..85c29521624 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -1,6 +1,8 @@ package de.uka.ilkd.key.settings; import java.util.*; +import java.util.stream.Collectors; +import javax.annotation.Nonnull; import de.uka.ilkd.key.logic.Choice; import de.uka.ilkd.key.logic.Name; @@ -11,10 +13,14 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; -public class ChoiceSettings implements Settings, Cloneable { +/** + * + */ +public class ChoiceSettings extends AbstractSettings { + private static final String KEY_DEFAULT_CHOICES = "[Choice]DefaultChoices"; - private static final String DEFAULTCHOICES_KEY = "[Choice]DefaultChoices"; - private final LinkedList listenerList = new LinkedList<>(); + private static final String PROP_CHOICE_DEFAULT = "category2Default"; + private static final String PROP_CHOICE_CATEGORIES = "category2Choices"; private HashMap category2Default; @@ -22,8 +28,7 @@ public class ChoiceSettings implements Settings, Cloneable { * maps categories to a set of Strings(representing the choices which are options for this * category). */ - private HashMap> category2Choices = - new LinkedHashMap<>(); + private Map> category2Choices = new LinkedHashMap<>(); public ChoiceSettings() { @@ -31,49 +36,47 @@ public ChoiceSettings() { } - public ChoiceSettings(HashMap category2Default) { - this.category2Default = category2Default; + public ChoiceSettings(Map category2Default) { + this.category2Default = new HashMap<>(category2Default); } - public void setDefaultChoices(HashMap category2Default) { - HashMap category2Defaultold = this.category2Default; - this.category2Default = category2Default; - if (category2Defaultold != null && !category2Defaultold.equals(category2Default)) { - fireSettingsChanged(); - } + public void setDefaultChoices(Map category2Default) { + var old = this.category2Default; + this.category2Default = new HashMap<>(category2Default); + firePropertyChange(PROP_CHOICE_DEFAULT, old, this.category2Default); } /** - * returns a copy of the HashMap that maps categories to their choices. + * returns a copy of the HashMap that maps categories to + * their choices. */ - @SuppressWarnings("unchecked") - public HashMap> getChoices() { - return (HashMap>) category2Choices.clone(); + public Map> getChoices() { + return Collections.unmodifiableMap(category2Choices); } - /** - * returns a copy of the HashMap that maps categories to their currently selected choices. - * + * Returns an immutable view of the current mapping between category and default choices. + *

* The method name is somewhat misleading. */ - @SuppressWarnings("unchecked") - public HashMap getDefaultChoices() { - return (HashMap) category2Default.clone(); + @Nonnull + public Map getDefaultChoices() { + return Collections.unmodifiableMap(category2Default); } /** - * returns the current selected choices as set + * returns the current selected choices as an immutable set */ + @Nonnull public ImmutableSet getDefaultChoicesAsSet() { return choiceMap2choiceSet(category2Default); } - private static ImmutableSet choiceMap2choiceSet(HashMap ccc) { + private static ImmutableSet choiceMap2choiceSet(Map ccc) { ImmutableList choices = ImmutableSLList.nil(); for (final Map.Entry entry : ccc.entrySet()) { choices = choices.prepend(new Choice(new Name(entry.getValue()), entry.getKey())); @@ -81,6 +84,11 @@ private static ImmutableSet choiceMap2choiceSet(HashMap return DefaultImmutableSet.fromImmutableList(choices); } + private void setChoiceCategories(HashMap> c2C) { + var old = category2Choices; + this.category2Choices = new HashMap<>(c2C); + firePropertyChange(PROP_CHOICE_CATEGORIES, old, category2Choices); + } /** * updates category2Choices if new entries are found in choiceNS or if @@ -89,64 +97,46 @@ private static ImmutableSet choiceMap2choiceSet(HashMap * @param remove remove entries not present in choiceNS */ public void updateChoices(Namespace choiceNS, boolean remove) { - Iterator it = choiceNS.allElements().iterator(); + // Translate the given namespace into a map of 'string -> list[string]' HashMap> c2C = new LinkedHashMap<>(); - Choice c; - Set soc; - while (it.hasNext()) { - c = it.next(); - if (c2C.containsKey(c.category())) { - soc = c2C.get(c.category()); - soc.add(c.name().toString()); - c2C.put(c.category(), soc); - } else { - soc = new LinkedHashSet<>(); - soc.add(c.name().toString()); - c2C.put(c.category(), soc); - } + for (Choice c : choiceNS.allElements()) { + Set soc = c2C.computeIfAbsent(c.category(), k -> new LinkedHashSet<>()); + soc.add(c.name().toString()); } + + // if there differences in the stored defaults, changed it accordingly if (!c2C.equals(category2Choices)) { - if (remove) { - category2Choices = c2C; - fireSettingsChanged(); + var tmp = new HashMap<>(category2Choices); + if (!remove) { + tmp.putAll(c2C); + setChoiceCategories(tmp); } else { - category2Choices.putAll(c2C); - ProofSettings.DEFAULT_SETTINGS.saveSettings(); + setChoiceCategories(c2C); } } - for (final String s : getDefaultChoices().keySet()) { + + var defaultTmp = new HashMap<>(category2Default); + for (var pair : category2Default.entrySet()) { + var s = pair.getKey(); + var v = pair.getValue(); + // if key is known then the default value should exist if (category2Choices.containsKey(s)) { - if (!category2Choices.get(s).contains(category2Default.get(s))) { - category2Default.put(s, category2Choices.get(s).iterator().next()); - fireSettingsChanged(); + if (!category2Choices.get(s).contains(v)) { + defaultTmp.put(s, category2Choices.get(s).iterator().next()); } } else { - category2Default.remove(s); - fireSettingsChanged(); + defaultTmp.remove(s); } } + setDefaultChoices(defaultTmp); } - - /** - * sends the message that the state of this setting has been changed to its registered listeners - * (not thread-safe) - */ - protected void fireSettingsChanged() { - Iterator it = listenerList.iterator(); - ProofSettings.DEFAULT_SETTINGS.saveSettings(); - while (it.hasNext()) { - it.next().settingsChanged(new EventObject(this)); - } - } - - /** * gets a Properties object and has to perform the necessary steps in order to change this * object in a way that it represents the stored settings */ public void readSettings(Properties props) { - String choiceSequence = props.getProperty(DEFAULTCHOICES_KEY); + String choiceSequence = props.getProperty(KEY_DEFAULT_CHOICES); // set choices if (choiceSequence != null) { StringTokenizer st = new StringTokenizer(choiceSequence, ","); @@ -163,21 +153,19 @@ public void readSettings(Properties props) { /** * implements the method required by the Settings interface. The settings are written to the - * given Properties object. Only entries of the form < key > = < value > (,< + * given Properties object. Only entries of + * the form < key > = < value > (,< * value >)* are allowed. * - * @param props the Properties object where to write the settings as (key, value) pair + ** @param props the Properties object where to write the + * settings as (key, value) pair */ + @Override public void writeSettings(Properties props) { - StringBuilder choiceSequence = new StringBuilder(); - var keys = category2Default.keySet().stream().sorted().toArray(String[]::new); - for (var key : keys) { - if (choiceSequence.length() > 0) { - choiceSequence.append(", "); - } - choiceSequence.append(key).append("-").append(category2Default.get(key)); - } - props.setProperty(DEFAULTCHOICES_KEY, choiceSequence.toString()); + var choiceSequence = category2Default.entrySet().stream() + .map(entry -> entry.getKey() + "-" + entry.getValue()) + .collect(Collectors.joining(" , ")); + props.setProperty(KEY_DEFAULT_CHOICES, choiceSequence); } @@ -187,19 +175,4 @@ public ChoiceSettings updateWith(Iterable sc) { } return this; } - - - /** - * adds a listener to the settings object - * - * @param l the listener - */ - public void addSettingsListener(SettingsListener l) { - listenerList.add(l); - } - - @Override - public void removeSettingsListener(SettingsListener l) { - listenerList.remove(l); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/DefaultSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/DefaultSMTSettings.java index 6dca123b5c1..d3d9ec1da40 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/DefaultSMTSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/DefaultSMTSettings.java @@ -1,6 +1,7 @@ package de.uka.ilkd.key.settings; +import java.beans.PropertyChangeListener; import java.io.File; import java.util.Collection; import java.util.LinkedList; @@ -62,7 +63,7 @@ public int getMaxConcurrentProcesses() { @Override public int getMaxNumberOfGenerics() { - return pdSettings.maxGenericSorts; + return pdSettings.getMaxGenericSorts(); } @Override @@ -79,7 +80,7 @@ public Collection getTaclets() { } for (Taclet taclet : proof.getInitConfig().activatedTaclets()) { - if (pdSettings.supportedTaclets.contains(taclet.name().toString(), true)) { + if (pdSettings.getSupportedTaclets().contains(taclet.name().toString(), true)) { taclets.add(taclet); } } @@ -104,7 +105,7 @@ public long getTimeout(SolverType type) { @Override public boolean instantiateNullAssumption() { - return pdSettings.useNullInstantiation; + return pdSettings.isUseNullInstantiation(); } @Override @@ -118,29 +119,29 @@ public boolean makesUseOfTaclets() { @Override public boolean useAssumptionsForBigSmallIntegers() { - return pdSettings.useConstantsForIntegers; + return pdSettings.isUseConstantsForIntegers(); } @Override public boolean useBuiltInUniqueness() { - return pdSettings.useBuiltInUniqueness; + return pdSettings.isUseBuiltInUniqueness(); } @Override public boolean useExplicitTypeHierarchy() { - return pdSettings.useExplicitTypeHierarchy; + return pdSettings.isUseExplicitTypeHierarchy(); } @Override public boolean useUninterpretedMultiplicationIfNecessary() { - return pdSettings.useUIMultiplication; + return pdSettings.isUseUIMultiplication(); } public SupportedTaclets getSupportedTaclets() { - return pdSettings.supportedTaclets; + return pdSettings.getSupportedTaclets(); } public ProofIndependentSMTSettings.ProgressMode getModeOfProgressDialog() { @@ -163,24 +164,19 @@ public String getPathForSMTTranslation() { return piSettings.getPathForSMTTranslation(); } - public void fireSettingsChanged() { - piSettings.fireSettingsChanged(); - pdSettings.fireSettingsChanged(); - } - - public void addListener(SettingsListener listener) { - piSettings.addSettingsListener(listener); - pdSettings.addSettingsListener(listener); + public void addListener(PropertyChangeListener listener) { + piSettings.addPropertyChangeListener(listener); + pdSettings.addPropertyChangeListener(listener); } @Override public long getMaximumInteger() { - return pdSettings.maxInteger; + return pdSettings.getMaxInteger(); } @Override public long getMinimumInteger() { - return pdSettings.minInteger; + return pdSettings.getMinInteger(); } @Override @@ -221,7 +217,7 @@ public long getLocSetBound() { @Override public boolean invarianForall() { - return pdSettings.invariantForall; + return pdSettings.isInvariantForall(); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java index 71af6833700..2d12afae156 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java @@ -1,13 +1,9 @@ package de.uka.ilkd.key.settings; -import java.util.EventObject; -import java.util.LinkedList; import java.util.Properties; -import de.uka.ilkd.key.proof.io.AutoSaver; - -public class GeneralSettings implements Settings, Cloneable { +public class GeneralSettings extends AbstractSettings { /** * This parameter disables the possibility to prune in closed branches. It is meant as a * fallback solution if storing all closed goals needs too much memory or is not needed. Pruning @@ -27,25 +23,37 @@ public class GeneralSettings implements Settings, Cloneable { * regular settings */ public static boolean disableSpecs = false; + + private static final String TACLET_FILTER = "[General]StupidMode"; private static final String DND_DIRECTION_SENSITIVE_KEY = "[General]DnDDirectionSensitive"; private static final String USE_JML_KEY = "[General]UseJML"; private static final String RIGHT_CLICK_MACROS_KEY = "[General]RightClickMacros"; private static final String AUTO_SAVE = "[General]AutoSavePeriod"; - /** The key for storing the ensureSourceConsistency flag in settings */ + /** + * The key for storing the ensureSourceConsistency flag in settings + */ private static final String ENSURE_SOURCE_CONSISTENCY = "[General]EnsureSourceConsistency"; - /** minimize interaction is on by default */ + /** + * minimize interaction is on by default + */ private boolean tacletFilter = true; - /** is drag and drop instantiation direction sensitive */ + /** + * is drag and drop instantiation direction sensitive + */ private boolean dndDirectionSensitive = true; - /** launches the rightclick the macro menu. on by default. */ + /** + * launches the rightclick the macro menu. on by default. + */ private boolean rightClickMacros = true; - /** JML is active by default */ + /** + * JML is active by default + */ private boolean useJML = true; /** @@ -59,14 +67,12 @@ public class GeneralSettings implements Settings, Cloneable { */ private boolean ensureSourceConsistency = true; - private final LinkedList listenerList = new LinkedList<>(); - GeneralSettings() { - addSettingsListener(AutoSaver.settingsListener); + // addSettingsListener(AutoSaver.settingsListener); } // getter - public boolean tacletFilter() { + public boolean getTacletFilter() { return tacletFilter; } @@ -78,7 +84,7 @@ public boolean isRightClickMacro() { return rightClickMacros; } - public boolean useJML() { + public boolean isUseJML() { return useJML && !disableSpecs; } @@ -92,36 +98,33 @@ public boolean isEnsureSourceConsistency() { // setter public void setTacletFilter(boolean b) { - if (tacletFilter != b) { - tacletFilter = b; - fireSettingsChanged(); - } + var old = tacletFilter; + tacletFilter = b; + firePropertyChange(TACLET_FILTER, old, b); } public void setDnDDirectionSensitivity(boolean b) { - if (dndDirectionSensitive != b) { - dndDirectionSensitive = b; - fireSettingsChanged(); - } + var old = dndDirectionSensitive; + dndDirectionSensitive = b; + firePropertyChange(DND_DIRECTION_SENSITIVE_KEY, old, dndDirectionSensitive); } public void setRightClickMacros(boolean b) { - if (this.rightClickMacros != b) { - rightClickMacros = b; - fireSettingsChanged(); - } + var old = rightClickMacros; + rightClickMacros = b; + firePropertyChange(RIGHT_CLICK_MACROS_KEY, old, rightClickMacros); } public void setUseJML(boolean b) { - if (useJML != b) { - useJML = b; - fireSettingsChanged(); - } + var old = useJML; + useJML = b; + firePropertyChange(USE_JML_KEY, old, useJML); } public void setAutoSave(int period) { + var old = autoSave; autoSave = period; - fireSettingsChanged(); + firePropertyChange(AUTO_SAVE, old, autoSave); } /** @@ -131,10 +134,9 @@ public void setAutoSave(int period) { * @param b the new truth value of the flag */ public void setEnsureSourceConsistency(boolean b) { - if (ensureSourceConsistency != b) { - ensureSourceConsistency = b; - fireSettingsChanged(); - } + var old = ensureSourceConsistency; + ensureSourceConsistency = b; + firePropertyChange(ENSURE_SOURCE_CONSISTENCY, old, ensureSourceConsistency); } /** @@ -144,7 +146,7 @@ public void setEnsureSourceConsistency(boolean b) { public void readSettings(Properties props) { String val = props.getProperty(TACLET_FILTER); if (val != null) { - tacletFilter = Boolean.parseBoolean(val); + setTacletFilter(Boolean.parseBoolean(val)); } val = props.getProperty(DND_DIRECTION_SENSITIVE_KEY); @@ -154,38 +156,40 @@ public void readSettings(Properties props) { val = props.getProperty(RIGHT_CLICK_MACROS_KEY); if (val != null) { - rightClickMacros = Boolean.parseBoolean(val); + setRightClickMacros(Boolean.parseBoolean(val)); } val = props.getProperty(USE_JML_KEY); if (val != null) { - useJML = Boolean.parseBoolean(val); + setUseJML(Boolean.parseBoolean(val)); } val = props.getProperty(AUTO_SAVE); if (val != null) { try { - autoSave = Integer.parseInt(val); + setAutoSave(Integer.parseInt(val)); if (autoSave < 0) { - autoSave = 0; + setAutoSave(0); } } catch (NumberFormatException e) { - autoSave = 0; + setAutoSave(0); } } val = props.getProperty(ENSURE_SOURCE_CONSISTENCY); if (val != null) { - ensureSourceConsistency = Boolean.parseBoolean(val); + setEnsureSourceConsistency(Boolean.parseBoolean(val)); } } /** * implements the method required by the Settings interface. The settings are written to the - * given Properties object. Only entries of the form = (,)* are allowed. + * given Properties object. Only entries of the form + * = (,)* are allowed. * * @param props the Properties object where to write the settings as (key, value) pair */ + @Override public void writeSettings(Properties props) { props.setProperty(TACLET_FILTER, String.valueOf(tacletFilter)); props.setProperty(DND_DIRECTION_SENSITIVE_KEY, String.valueOf(dndDirectionSensitive)); @@ -194,32 +198,4 @@ public void writeSettings(Properties props) { props.setProperty(AUTO_SAVE, String.valueOf(autoSave)); props.setProperty(ENSURE_SOURCE_CONSISTENCY, String.valueOf(ensureSourceConsistency)); } - - /** - * sends the message that the state of this setting has been changed to its registered listeners - * (not thread-safe) - */ - protected void fireSettingsChanged() { - for (SettingsListener aListenerList : listenerList) { - aListenerList.settingsChanged(new EventObject(this)); - } - } - - /** - * adds a listener to the settings object - * - * @param l the listener - */ - public void addSettingsListener(SettingsListener l) { - listenerList.add(l); - } - - /** - * removes the listener from the settings object - * - * @param l the listener to remove - */ - public void removeSettingsListener(SettingsListener l) { - listenerList.remove(l); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java index 682a37d0393..da11a755873 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java @@ -1,66 +1,45 @@ package de.uka.ilkd.key.settings; -import java.util.EventObject; -import java.util.LinkedList; import java.util.Properties; -public class LemmaGeneratorSettings implements de.uka.ilkd.key.settings.Settings, Cloneable { - private final LinkedList listeners = new LinkedList<>(); - private boolean showDialogAddingAxioms = true; - private boolean showDialogUsingAxioms = true; +public class LemmaGeneratorSettings extends AbstractSettings { private static final String SHOW_DIALOG_ADDING_AXIOMS = "[LemmaGenerator]showDialogWhenAddingAxioms"; private static final String SHOW_DIALOG_USING_AXIOMS = "[LemmaGenerator]showDialogWhenUsingTacletsAsAxioms"; - - - private void fireSettingsChanged() { - for (SettingsListener listener : listeners) { - listener.settingsChanged(new EventObject(this)); - } - } - + private boolean showDialogAddingAxioms = true; + private boolean showDialogUsingAxioms = true; public boolean isShowingDialogAddingAxioms() { return showDialogAddingAxioms; } - public void showDialogAddingAxioms(boolean value) { + public void setShowDialogAddingAxioms(boolean value) { + var old = this.showDialogAddingAxioms; this.showDialogAddingAxioms = value; - fireSettingsChanged(); + firePropertyChange(SHOW_DIALOG_USING_AXIOMS, old, showDialogUsingAxioms); } public boolean isShowingDialogUsingAxioms() { return showDialogUsingAxioms; } - public void showDialogUsingAxioms(boolean value) { + public void setShowDialogUsingAxioms(boolean value) { + var old = this.showDialogUsingAxioms; this.showDialogUsingAxioms = value; - fireSettingsChanged(); - } - - @Override - public void addSettingsListener(SettingsListener l) { - listeners.add(l); - } - - @Override - public void removeSettingsListener(SettingsListener l) { - listeners.remove(l); + firePropertyChange(SHOW_DIALOG_USING_AXIOMS, old, showDialogUsingAxioms); } @Override public void readSettings(Properties props) { - showDialogAddingAxioms = SettingsConverter.read(props, SHOW_DIALOG_ADDING_AXIOMS, true); - showDialogUsingAxioms = SettingsConverter.read(props, SHOW_DIALOG_USING_AXIOMS, true); + setShowDialogAddingAxioms(SettingsConverter.read(props, SHOW_DIALOG_ADDING_AXIOMS, true)); + setShowDialogUsingAxioms(SettingsConverter.read(props, SHOW_DIALOG_USING_AXIOMS, true)); } @Override public void writeSettings(Properties props) { SettingsConverter.store(props, SHOW_DIALOG_ADDING_AXIOMS, showDialogAddingAxioms); SettingsConverter.store(props, SHOW_DIALOG_USING_AXIOMS, showDialogUsingAxioms); - } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java index 89f3ca80186..8ede3adef87 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java @@ -2,10 +2,7 @@ import java.util.Collections; -import java.util.EventObject; import java.util.LinkedHashMap; -import java.util.LinkedList; -import java.util.List; import java.util.Map; import java.util.Map.Entry; import java.util.Objects; @@ -25,16 +22,13 @@ * * @author Mattias Ulbrich */ -public class NewSMTTranslationSettings implements Settings, Cloneable { - +public class NewSMTTranslationSettings extends AbstractSettings { private static final String PREFIX = "[NewSMT]"; // Using a linked hash map to make the order deterministic in writing to // file private final Map map = new LinkedHashMap<>(); - private final List listeners = new LinkedList<>(); - /** * Creates a new settings object in which no option is set. */ @@ -110,26 +104,12 @@ public String get(String key) { * @return the value that was in the map prior to the call (see {@link Map#put(Object, Object)}. */ public String put(String key, String value) { + var old = map.get(key); String result = map.put(Objects.requireNonNull(key), Objects.requireNonNull(value)); - for (SettingsListener listener : listeners) { - listener.settingsChanged(new EventObject(this)); - } + firePropertyChange(key, old, value); return result; } - @Override - public void addSettingsListener(SettingsListener l) { - listeners.add(l); - } - - @Override - public void removeSettingsListener(SettingsListener l) { - listeners.remove(l); - } - - /** - * see {@link SMTSettings#copy(SMTSettings)} - */ public void copy(NewSMTTranslationSettings newTranslationSettings) { this.map.clear(); this.map.putAll(newTranslationSettings.map); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java index bdf1f358a72..9599b2da244 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java @@ -1,63 +1,46 @@ package de.uka.ilkd.key.settings; -import java.util.Collection; -import java.util.EventObject; -import java.util.LinkedHashSet; import java.util.Properties; import de.uka.ilkd.key.taclettranslation.assumptions.SupportedTaclets; +public class ProofDependentSMTSettings extends AbstractSettings { -public class ProofDependentSMTSettings implements de.uka.ilkd.key.settings.Settings, Cloneable { - - private static final String EXPLICIT_TYPE_HIERARCHY = "[SMTSettings]explicitTypeHierarchy"; - - private static final String INSTANTIATE_NULL_PREDICATES = + public static final String EXPLICIT_TYPE_HIERARCHY = "[SMTSettings]explicitTypeHierarchy"; + public static final String INSTANTIATE_NULL_PREDICATES = "[SMTSettings]instantiateHierarchyAssumptions"; - - - private static final String MAX_GENERIC_SORTS = "[SMTSettings]maxGenericSorts"; - - - private static final String TACLET_SELECTION = "[SMTSettings]SelectedTaclets"; - - private static final String USE_BUILT_IN_UNIQUENESS = "[SMTSettings]UseBuiltUniqueness"; - - private static final String USE_UNINTERPRETED_MULTIPLICATION = + public static final String MAX_GENERIC_SORTS = "[SMTSettings]maxGenericSorts"; + public static final String TACLET_SELECTION = "[SMTSettings]SelectedTaclets"; + public static final String USE_BUILT_IN_UNIQUENESS = "[SMTSettings]UseBuiltUniqueness"; + public static final String USE_UNINTERPRETED_MULTIPLICATION = "[SMTSettings]useUninterpretedMultiplication"; - - private static final String USE_CONSTANTS_FOR_BIGSMALL_INTEGERS = + public static final String USE_CONSTANTS_FOR_BIGSMALL_INTEGERS = "[SMTSettings]useConstantsForBigOrSmallIntegers"; + public static final String INTEGERS_MAXIMUM = "[SMTSettings]integersMaximum"; + public static final String INTEGERS_MINIMUM = "[SMTSettings]integersMinimum"; + public static final String INVARIANT_FORALL = "[SMTSettings]invariantForall"; - private static final String INTEGERS_MAXIMUM = "[SMTSettings]integersMaximum"; - private static final String INTEGERS_MINIMUM = "[SMTSettings]integersMinimum"; - - private static final String INVARIANT_FORALL = "[SMTSettings]invariantForall"; - - private final Collection listeners = new LinkedHashSet<>(); - - // FIXME Why are these fields public?! - public boolean useExplicitTypeHierarchy = false; - public boolean useNullInstantiation = true; - public boolean useBuiltInUniqueness = false; - public boolean useUIMultiplication = true; - public boolean useConstantsForIntegers = true; - public boolean invariantForall = false; - public int maxGenericSorts = 2; - public long maxInteger = 2147483645; - public long minInteger = -2147483645; - // TODO js: could be used once the new translation is working - // public boolean useLegacyTranslation = false; + public static final String PROP_LEGACY_TRANSLATION = "[SMTSettings]legacyTranslation"; + private static final String PROP_SUPPORTED_TACLETS = "supportedTaclets"; + private boolean useExplicitTypeHierarchy = false; + private boolean useNullInstantiation = true; + private boolean useBuiltInUniqueness = false; + private boolean useUIMultiplication = true; + private boolean useConstantsForIntegers = true; + private boolean invariantForall = false; + private int maxGenericSorts = 2; + private long maxInteger = 2147483645; + private long minInteger = -2147483645; + private boolean useLegacyTranslation = false; - public SupportedTaclets supportedTaclets; + private SupportedTaclets supportedTaclets; private ProofDependentSMTSettings() { - - supportedTaclets = SupportedTaclets.REFERENCE; + setSupportedTaclets(SupportedTaclets.REFERENCE); } private ProofDependentSMTSettings(ProofDependentSMTSettings data) { @@ -65,17 +48,17 @@ private ProofDependentSMTSettings(ProofDependentSMTSettings data) { } public void copy(ProofDependentSMTSettings data) { - supportedTaclets = new SupportedTaclets(data.supportedTaclets.getNamesOfSelectedTaclets()); - this.useExplicitTypeHierarchy = data.useExplicitTypeHierarchy; - this.useNullInstantiation = data.useNullInstantiation; - this.maxGenericSorts = data.maxGenericSorts; - this.useBuiltInUniqueness = data.useBuiltInUniqueness; - this.useUIMultiplication = data.useUIMultiplication; - this.useConstantsForIntegers = data.useConstantsForIntegers; - this.maxInteger = data.maxInteger; - this.minInteger = data.minInteger; - this.invariantForall = data.invariantForall; - + setSupportedTaclets( + new SupportedTaclets(data.supportedTaclets.getNamesOfSelectedTaclets())); + setUseExplicitTypeHierarchy(data.useExplicitTypeHierarchy); + setUseNullInstantiation(data.useNullInstantiation); + setMaxGenericSorts(data.maxGenericSorts); + setUseBuiltInUniqueness(data.useBuiltInUniqueness); + setUseUIMultiplication(data.useUIMultiplication); + setUseConstantsForIntegers(data.useConstantsForIntegers); + setMaxInteger(data.maxInteger); + setMinInteger(data.minInteger); + setInvariantForall(data.invariantForall); } @@ -86,39 +69,35 @@ public static ProofDependentSMTSettings getDefaultSettingsData() { } - @Override public ProofDependentSMTSettings clone() { return new ProofDependentSMTSettings(this); } + @Override public void readSettings(Properties props) { - - useExplicitTypeHierarchy = - SettingsConverter.read(props, EXPLICIT_TYPE_HIERARCHY, useExplicitTypeHierarchy); - useNullInstantiation = - SettingsConverter.read(props, INSTANTIATE_NULL_PREDICATES, useNullInstantiation); - useBuiltInUniqueness = - SettingsConverter.read(props, USE_BUILT_IN_UNIQUENESS, useBuiltInUniqueness); - - maxGenericSorts = SettingsConverter.read(props, MAX_GENERIC_SORTS, maxGenericSorts); - - useUIMultiplication = - SettingsConverter.read(props, USE_UNINTERPRETED_MULTIPLICATION, useUIMultiplication); - useConstantsForIntegers = SettingsConverter.read(props, USE_CONSTANTS_FOR_BIGSMALL_INTEGERS, - useConstantsForIntegers); - - maxInteger = SettingsConverter.read(props, INTEGERS_MAXIMUM, maxInteger); - minInteger = SettingsConverter.read(props, INTEGERS_MINIMUM, minInteger); - - invariantForall = SettingsConverter.read(props, INVARIANT_FORALL, invariantForall); - + setUseExplicitTypeHierarchy( + SettingsConverter.read(props, EXPLICIT_TYPE_HIERARCHY, useExplicitTypeHierarchy)); + setUseNullInstantiation( + SettingsConverter.read(props, INSTANTIATE_NULL_PREDICATES, useNullInstantiation)); + setUseBuiltInUniqueness( + SettingsConverter.read(props, USE_BUILT_IN_UNIQUENESS, useBuiltInUniqueness)); + setMaxGenericSorts(SettingsConverter.read(props, MAX_GENERIC_SORTS, maxGenericSorts)); + setUseUIMultiplication( + SettingsConverter.read(props, USE_UNINTERPRETED_MULTIPLICATION, useUIMultiplication)); + setUseConstantsForIntegers( + SettingsConverter.read(props, USE_CONSTANTS_FOR_BIGSMALL_INTEGERS, + useConstantsForIntegers)); + + setMaxInteger(SettingsConverter.read(props, INTEGERS_MAXIMUM, maxInteger)); + setMinInteger(SettingsConverter.read(props, INTEGERS_MINIMUM, minInteger)); + setInvariantForall(SettingsConverter.read(props, INVARIANT_FORALL, invariantForall)); supportedTaclets.selectTaclets(SettingsConverter.read(props, TACLET_SELECTION, supportedTaclets.getNamesOfSelectedTaclets())); - } + @Override public void writeSettings(Properties props) { SettingsConverter.store(props, EXPLICIT_TYPE_HIERARCHY, useExplicitTypeHierarchy); SettingsConverter.store(props, INSTANTIATE_NULL_PREDICATES, useNullInstantiation); @@ -134,25 +113,113 @@ public void writeSettings(Properties props) { SettingsConverter.store(props, INVARIANT_FORALL, invariantForall); } + public boolean isUseExplicitTypeHierarchy() { + return useExplicitTypeHierarchy; + } - public void fireSettingsChanged() { - for (SettingsListener aListenerList : listeners) { - aListenerList.settingsChanged(new EventObject(this)); - } + public void setUseExplicitTypeHierarchy(boolean useExplicitTypeHierarchy) { + var old = this.useExplicitTypeHierarchy; + this.useExplicitTypeHierarchy = useExplicitTypeHierarchy; + firePropertyChange(EXPLICIT_TYPE_HIERARCHY, old, this.useExplicitTypeHierarchy); + } + public boolean isUseNullInstantiation() { + return useNullInstantiation; } - @Override - public void addSettingsListener(SettingsListener l) { - listeners.add(l); + public void setUseNullInstantiation(boolean useNullInstantiation) { + var old = this.useNullInstantiation; + this.useNullInstantiation = useNullInstantiation; + firePropertyChange(INSTANTIATE_NULL_PREDICATES, old, this.useNullInstantiation); + } + public boolean isUseBuiltInUniqueness() { + return useBuiltInUniqueness; } - @Override - public void removeSettingsListener(SettingsListener l) { - listeners.remove(l); + public void setUseBuiltInUniqueness(boolean useBuiltInUniqueness) { + var old = this.useBuiltInUniqueness; + this.useBuiltInUniqueness = useBuiltInUniqueness; + firePropertyChange(USE_BUILT_IN_UNIQUENESS, old, useBuiltInUniqueness); } + public boolean isUseUIMultiplication() { + return useUIMultiplication; + } + + public void setUseUIMultiplication(boolean useUIMultiplication) { + var old = this.useUIMultiplication; + this.useUIMultiplication = useUIMultiplication; + firePropertyChange(USE_UNINTERPRETED_MULTIPLICATION, old, useUIMultiplication); + } + + public boolean isUseConstantsForIntegers() { + return useConstantsForIntegers; + } + + public void setUseConstantsForIntegers(boolean useConstantsForIntegers) { + var old = this.useConstantsForIntegers; + this.useConstantsForIntegers = useConstantsForIntegers; + firePropertyChange(USE_CONSTANTS_FOR_BIGSMALL_INTEGERS, old, useConstantsForIntegers); + } + public boolean isInvariantForall() { + return invariantForall; + } + public void setInvariantForall(boolean invariantForall) { + var old = this.invariantForall; + this.invariantForall = invariantForall; + firePropertyChange(INVARIANT_FORALL, old, invariantForall); + } + + public int getMaxGenericSorts() { + return maxGenericSorts; + } + + public void setMaxGenericSorts(int maxGenericSorts) { + var old = this.maxGenericSorts; + this.maxGenericSorts = maxGenericSorts; + firePropertyChange(MAX_GENERIC_SORTS, old, maxGenericSorts); + } + + public long getMaxInteger() { + return maxInteger; + } + + public void setMaxInteger(long maxInteger) { + var old = this.maxInteger; + this.maxInteger = maxInteger; + firePropertyChange(INTEGERS_MAXIMUM, old, maxInteger); + } + + public long getMinInteger() { + return minInteger; + } + + public void setMinInteger(long minInteger) { + var old = this.minInteger; + this.minInteger = minInteger; + firePropertyChange(INTEGERS_MINIMUM, old, minInteger); + } + + public SupportedTaclets getSupportedTaclets() { + return supportedTaclets; + } + + public void setSupportedTaclets(SupportedTaclets supportedTaclets) { + var old = this.supportedTaclets; + this.supportedTaclets = supportedTaclets; + firePropertyChange(PROP_SUPPORTED_TACLETS, old, supportedTaclets); + } + + public boolean isUseLegacyTranslation() { + return useLegacyTranslation; + } + + public void setUseLegacyTranslation(boolean useLegacyTranslation) { + var old = this.useLegacyTranslation; + this.useLegacyTranslation = useLegacyTranslation; + firePropertyChange(PROP_LEGACY_TRANSLATION, old, useLegacyTranslation); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java index 62875033b25..277b3b016b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java @@ -8,45 +8,42 @@ import de.uka.ilkd.key.smt.solvertypes.SolverTypes; public final class ProofIndependentSMTSettings - implements de.uka.ilkd.key.settings.Settings, Cloneable { + extends AbstractSettings { - private static final String ACTIVE_SOLVER = "[SMTSettings]ActiveSolver"; - - private static final String KEY_TIMEOUT = "[SMTSettings]SolverTimeout"; - - - private static final String PATH_FOR_SMT_TRANSLATION = "[SMTSettings]pathForSMTTranslation"; - - private static final String PATH_FOR_TACLET_TRANSLATION = + public static final String ACTIVE_SOLVER = "[SMTSettings]ActiveSolver"; + public static final String KEY_TIMEOUT = "[SMTSettings]SolverTimeout"; + public static final String PATH_FOR_SMT_TRANSLATION = "[SMTSettings]pathForSMTTranslation"; + public static final String PATH_FOR_TACLET_TRANSLATION = "[SMTSettings]pathForTacletTranslation"; - - private static final String SHOW_SMT_RES_DIA = "[SMTSettings]showSMTResDialog"; - - - private static final String PROGRESS_DIALOG_MODE = "[SMTSettings]modeOfProgressDialog"; - - - private static final String MAX_CONCURRENT_PROCESSES = "[SMTSettings]maxConcurrentProcesses"; + public static final String SHOW_SMT_RES_DIA = "[SMTSettings]showSMTResDialog"; + public static final String PROGRESS_DIALOG_MODE = "[SMTSettings]modeOfProgressDialog"; + public static final String MAX_CONCURRENT_PROCESSES = "[SMTSettings]maxConcurrentProcesses"; /* * The following properties are used to set the bit sizes for bounded counter example * generation. */ - private static final String INT_BOUND = "[SMTSettings]intBound"; - private static final String HEAP_BOUND = "[SMTSettings]heapBound"; - private static final String FIELD_BOUND = "[SMTSettings]fieldBound"; - private static final String OBJECT_BOUND = "[SMTSettings]objectBound"; - private static final String LOCSET_BOUND = "[SMTSettings]locsetBound"; + public static final String INT_BOUND = "[SMTSettings]intBound"; + public static final String HEAP_BOUND = "[SMTSettings]heapBound"; + public static final String FIELD_BOUND = "[SMTSettings]fieldBound"; + public static final String OBJECT_BOUND = "[SMTSettings]objectBound"; + public static final String LOCSET_BOUND = "[SMTSettings]locsetBound"; - private static final String SOLVER_PARAMETERS = "[SMTSettings]solverParametersV1"; - private static final String SOLVER_COMMAND = "[SMTSettings]solverCommand"; - private static final String PROP_TIMEOUT = "[SMTSettings]timeout"; - private static final String SOLVER_CHECK_FOR_SUPPORT = "[SMTSettings]checkForSupport"; + public static final String SOLVER_PARAMETERS = "[SMTSettings]solverParametersV1"; + public static final String SOLVER_COMMAND = "[SMTSettings]solverCommand"; + public static final String PROP_TIMEOUT = "[SMTSettings]timeout"; + public static final String SOLVER_CHECK_FOR_SUPPORT = "[SMTSettings]checkForSupport"; private static final ProofIndependentSMTSettings DEFAULT_DATA = new ProofIndependentSMTSettings(); private static final int DEFAULT_BIT_LENGTH_FOR_CE_GENERATION = 3; + public static final String PROP_SOLVER_UNION = "activeSolverUnion"; + public static final String PROP_SHOW_RESULT_AFTER_EXECUTION = + "PROP_SHOW_RESULT_AFTER_EXECUTION"; + public static final String PROP_STORE_SMT_TRANSLATION_FILE = "PROP_STORE_SMT_TRANSLATION_FILE"; + public static final String PROP_STORE_TACLET_TRANSLATION_FILE = + "PROP_STORE_TACLET_TRANSLATION_FILE"; private final Collection solverTypes = new LinkedList<>(); private boolean showResultsAfterExecution = false; @@ -69,8 +66,6 @@ public final class ProofIndependentSMTSettings private long objectBound = DEFAULT_BIT_LENGTH_FOR_CE_GENERATION; private long locsetBound = DEFAULT_BIT_LENGTH_FOR_CE_GENERATION; - private final Collection listeners = new LinkedHashSet<>(); - private SolverTypeCollection activeSolverUnion = SolverTypeCollection.EMPTY_COLLECTION; private LinkedList solverUnions = new LinkedList<>(); private LinkedList legacyTranslationSolverUnions = new LinkedList<>(); @@ -109,7 +104,10 @@ public boolean isShowResultsAfterExecution() { } public void setShowResultsAfterExecution(boolean showResultsAfterExecution) { + var old = this.showResultsAfterExecution; this.showResultsAfterExecution = showResultsAfterExecution; + firePropertyChange(PROP_SHOW_RESULT_AFTER_EXECUTION, old, this.showResultsAfterExecution); + } public boolean isStoreSMTTranslationToFile() { @@ -117,7 +115,10 @@ public boolean isStoreSMTTranslationToFile() { } public void setStoreSMTTranslationToFile(boolean storeSMTTranslationToFile) { + var old = this.storeSMTTranslationToFile; this.storeSMTTranslationToFile = storeSMTTranslationToFile; + firePropertyChange(PROP_STORE_SMT_TRANSLATION_FILE, old, this.storeSMTTranslationToFile); + } public boolean isStoreTacletTranslationToFile() { @@ -125,7 +126,11 @@ public boolean isStoreTacletTranslationToFile() { } public void setStoreTacletTranslationToFile(boolean storeTacletTranslationToFile) { + var old = this.storeTacletTranslationToFile; this.storeTacletTranslationToFile = storeTacletTranslationToFile; + firePropertyChange(PROP_STORE_TACLET_TRANSLATION_FILE, old, + this.storeTacletTranslationToFile); + } public long getTimeout() { @@ -133,7 +138,10 @@ public long getTimeout() { } public void setTimeout(long timeout) { + var old = this.timeout; this.timeout = timeout; + firePropertyChange(PROP_TIMEOUT, old, this.timeout); + } public ProgressMode getModeOfProgressDialog() { @@ -141,7 +149,10 @@ public ProgressMode getModeOfProgressDialog() { } public void setModeOfProgressDialog(ProgressMode modeOfProgressDialog) { + var old = this.modeOfProgressDialog; this.modeOfProgressDialog = modeOfProgressDialog; + firePropertyChange(PROGRESS_DIALOG_MODE, old, this.modeOfProgressDialog); + } public String getPathForSMTTranslation() { @@ -149,7 +160,10 @@ public String getPathForSMTTranslation() { } public void setPathForSMTTranslation(String pathForSMTTranslation) { + var old = this.pathForSMTTranslation; this.pathForSMTTranslation = pathForSMTTranslation; + firePropertyChange(PATH_FOR_SMT_TRANSLATION, old, this.pathForSMTTranslation); + } public String getPathForTacletTranslation() { @@ -157,7 +171,10 @@ public String getPathForTacletTranslation() { } public void setPathForTacletTranslation(String pathForTacletTranslation) { + var old = this.pathForTacletTranslation; this.pathForTacletTranslation = pathForTacletTranslation; + firePropertyChange(PATH_FOR_TACLET_TRANSLATION, old, this.pathForTacletTranslation); + } public String getActiveSolver() { @@ -165,7 +182,10 @@ public String getActiveSolver() { } public void setActiveSolver(String activeSolver) { + var old = this.activeSolver; this.activeSolver = activeSolver; + firePropertyChange(ACTIVE_SOLVER, old, this.activeSolver); + } public long getIntBound() { @@ -173,7 +193,10 @@ public long getIntBound() { } public void setIntBound(long intBound) { + var old = this.intBound; this.intBound = intBound; + firePropertyChange(INT_BOUND, old, this.intBound); + } public long getHeapBound() { @@ -181,7 +204,10 @@ public long getHeapBound() { } public void setHeapBound(long heapBound) { + var old = this.heapBound; this.heapBound = heapBound; + firePropertyChange(HEAP_BOUND, old, this.heapBound); + } public long getSeqBound() { @@ -189,7 +215,10 @@ public long getSeqBound() { } public void setSeqBound(long seqBound) { + var old = this.seqBound; this.seqBound = seqBound; + firePropertyChange(FIELD_BOUND, old, this.seqBound); + } public long getObjectBound() { @@ -197,7 +226,10 @@ public long getObjectBound() { } public void setObjectBound(long objectBound) { + var old = this.objectBound; this.objectBound = objectBound; + firePropertyChange(OBJECT_BOUND, old, this.objectBound); + } public long getLocsetBound() { @@ -205,7 +237,10 @@ public long getLocsetBound() { } public void setLocsetBound(long locsetBound) { + var old = this.locsetBound; this.locsetBound = locsetBound; + firePropertyChange(LOCSET_BOUND, old, this.locsetBound); + } public boolean isCheckForSupport() { @@ -213,38 +248,45 @@ public boolean isCheckForSupport() { } public void setCheckForSupport(boolean checkForSupport) { + var old = this.checkForSupport; this.checkForSupport = checkForSupport; + firePropertyChange(SOLVER_CHECK_FOR_SUPPORT, old, this.checkForSupport); } public enum ProgressMode { USER, CLOSE, CLOSE_FIRST } + private final Map dataOfSolvers = new LinkedHashMap<>(); + public int getMaxConcurrentProcesses() { return maxConcurrentProcesses; } public void setMaxConcurrentProcesses(int maxConcurrentProcesses) { + var old = this.maxConcurrentProcesses; this.maxConcurrentProcesses = maxConcurrentProcesses; + firePropertyChange(MAX_CONCURRENT_PROCESSES, old, this.maxConcurrentProcesses); + } public void copy(ProofIndependentSMTSettings data) { - this.showResultsAfterExecution = data.showResultsAfterExecution; - this.storeSMTTranslationToFile = data.storeSMTTranslationToFile; - this.storeTacletTranslationToFile = data.storeTacletTranslationToFile; - this.timeout = data.timeout; - this.maxConcurrentProcesses = data.maxConcurrentProcesses; - this.pathForSMTTranslation = data.pathForSMTTranslation; - this.pathForTacletTranslation = data.pathForTacletTranslation; - this.modeOfProgressDialog = data.modeOfProgressDialog; - this.checkForSupport = data.checkForSupport; - this.intBound = data.intBound; - this.heapBound = data.heapBound; - this.seqBound = data.seqBound; - this.locsetBound = data.locsetBound; - this.objectBound = data.objectBound; + setShowResultsAfterExecution(data.showResultsAfterExecution); + setStoreSMTTranslationToFile(data.storeSMTTranslationToFile); + setStoreTacletTranslationToFile(data.storeTacletTranslationToFile); + setTimeout(data.timeout); + setMaxConcurrentProcesses(data.maxConcurrentProcesses); + setPathForSMTTranslation(data.pathForSMTTranslation); + setPathForTacletTranslation(data.pathForTacletTranslation); + setModeOfProgressDialog(data.modeOfProgressDialog); + setCheckForSupport(data.checkForSupport); + setIntBound(data.intBound); + setHeapBound(data.heapBound); + setSeqBound(data.seqBound); + setLocsetBound(data.locsetBound); + setObjectBound(data.objectBound); solverTypes.addAll(data.solverTypes); @@ -342,11 +384,10 @@ public void writeSettings(Properties props) { } public void setActiveSolverUnion(SolverTypeCollection solverUnion) { - if (activeSolverUnion != solverUnion) { - activeSolverUnion = solverUnion; - activeSolver = activeSolverUnion.name(); - fireSettingsChanged(); - } + var oldActiveSolverUnion = activeSolverUnion; + activeSolverUnion = solverUnion; + firePropertyChange(PROP_SOLVER_UNION, oldActiveSolverUnion, activeSolver); + setActiveSolver(activeSolverUnion.name()); } public SolverTypeCollection computeActiveSolverUnion() { @@ -391,21 +432,95 @@ public Collection getSolverUnions(boolean experimental) { return res; } - public void fireSettingsChanged() { - for (SettingsListener aListenerList : listeners) { - aListenerList.settingsChanged(new EventObject(this)); + public static class SolverData extends AbstractSettings { + private String solverParameters = ""; + private String solverCommand = ""; + private long timeout = -1; + private final SolverType type; + + public SolverData(SolverType type) { + this(type, type.getDefaultSolverCommand(), type.getDefaultSolverParameters()); } - } + private SolverData(SolverType type, String command, String parameters) { + this(type, command, parameters, -1); + } - @Override - public void addSettingsListener(SettingsListener l) { - listeners.add(l); - } + public SolverData(SolverType type, String command, String parameters, long timeout) { + this.type = type; + setSolverCommand(command); + setSolverParameters(parameters); + setTimeout(timeout); + } - @Override - public void removeSettingsListener(SettingsListener l) { - listeners.remove(l); - } + @Override + public void readSettings(Properties props) { + setSolverParameters(SettingsConverter.read(props, + SOLVER_PARAMETERS + getType().getName(), getSolverParameters())); + setTimeout( + SettingsConverter.read(props, PROP_TIMEOUT + getType().getName(), getTimeout())); + setSolverCommand(SettingsConverter.read(props, + SOLVER_COMMAND + getType().getName(), getSolverCommand())); + getType().setSolverParameters(getSolverParameters()); + getType().setSolverCommand(getSolverCommand()); + + } + + @Override + public void writeSettings(Properties props) { + SettingsConverter.store(props, SOLVER_PARAMETERS + getType().getName(), + getSolverParameters()); + SettingsConverter.store(props, SOLVER_COMMAND + getType().getName(), + getSolverCommand()); + SettingsConverter.store(props, PROP_TIMEOUT + getType().getName(), getTimeout()); + getType().setSolverParameters(getSolverParameters()); + getType().setSolverCommand(getSolverCommand()); + } + + + public SolverData clone() { + return new SolverData(getType(), getSolverCommand(), getSolverParameters(), + getTimeout()); + } + + public String toString() { + return getType().getName(); + } + + public String getSolverParameters() { + return solverParameters; + } + public void setSolverParameters(String solverParameters) { + var old = this.solverParameters; + this.solverParameters = solverParameters; + firePropertyChange(SOLVER_PARAMETERS, old, this.solverParameters); + + } + + public String getSolverCommand() { + return solverCommand; + } + + public void setSolverCommand(String solverCommand) { + var old = this.solverCommand; + this.solverCommand = solverCommand; + firePropertyChange(SOLVER_COMMAND, old, this.solverCommand); + + } + + public SolverType getType() { + return type; + } + + public long getTimeout() { + return timeout; + } + + public void setTimeout(long timeout) { + var old = this.timeout; + this.timeout = timeout; + firePropertyChange(KEY_TIMEOUT, old, this.timeout); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index a738015b8d3..5c5d0bbcdd1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.settings; +import java.beans.PropertyChangeListener; import java.io.File; import java.io.FileInputStream; import java.io.FileOutputStream; @@ -40,7 +41,7 @@ public class ProofIndependentSettings { private final List settings = new LinkedList<>(); - private final SettingsListener settingsListener = e -> saveSettings(); + private final PropertyChangeListener settingsListener = e -> saveSettings(); private Properties lastReadedProperties; private ProofIndependentSettings(String filename) { @@ -55,7 +56,7 @@ private ProofIndependentSettings(String filename) { public void addSettings(Settings settings) { if (!this.settings.contains(settings)) { this.settings.add(settings); - settings.addSettingsListener(settingsListener); + settings.addPropertyChangeListener(settingsListener); if (lastReadedProperties != null) { settings.readSettings(lastReadedProperties); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index 2a815c07ad8..66d3a29c790 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.settings; +import java.beans.PropertyChangeListener; import java.io.*; import java.net.URL; import java.nio.charset.StandardCharsets; @@ -51,28 +52,17 @@ private static ProofSettings loadedSettings() { /** * the default listener to settings */ - private final SettingsListener listener = e -> saveSettings(); - - // NOTE: This was commented out in commit - // 4932e4d1210356455c04a1e9fb7f2fa1f21b3e9d, 2012/11/08, in the process of - // separating proof independent from proof dependent settings. - // Is not in ProofIndependentSettings. I don't know why these code - // corpses have been left here as comments, therefore I don't removed them. - // (DS, 2017-05-11) - - // private final static int strategySettings = 0; - // private final static int GENERAL_SETTINGS = 1; - // private final static int choiceSettings = 2; - // private final static int smtSettings = 3; - // private final static int VIEW_SETTINGS = 4; + private final PropertyChangeListener listener = e -> saveSettings(); + private final StrategySettings strategySettings = new StrategySettings(); private final ChoiceSettings choiceSettings = new ChoiceSettings(); private final ProofDependentSMTSettings smtSettings = ProofDependentSMTSettings.getDefaultSettingsData(); private final NewSMTTranslationSettings newSMTSettings = new NewSMTTranslationSettings(); - private Properties lastLoadedProperties = null; private final TermLabelSettings termLabelSettings = new TermLabelSettings(); + private Properties lastLoadedProperties = null; + /** * create a proof settings object. When you add a new settings object, PLEASE UPDATE THE LIST * ABOVE AND USE THOSE CONSTANTS INSTEAD OF USING INTEGERS DIRECTLY @@ -103,7 +93,7 @@ public ProofSettings(ProofSettings toCopy) { public void addSettings(Settings settings) { this.settings.add(settings); - settings.addSettingsListener(listener); + settings.addPropertyChangeListener(listener); if (lastLoadedProperties != null) { settings.readSettings(lastLoadedProperties); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java index 6dfc3ea9f52..988c9042465 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java @@ -1,5 +1,6 @@ package de.uka.ilkd.key.settings; +import java.beans.PropertyChangeListener; import java.util.Properties; /** @@ -21,17 +22,13 @@ public interface Settings { */ void writeSettings(Properties props); - /** - * adds a listener to the settings object - * - * @param l the listener - */ - void addSettingsListener(SettingsListener l); + void addPropertyChangeListener(PropertyChangeListener listener); - /** - * removes a listener to the settings object - * - * @param l the listener - */ - void removeSettingsListener(SettingsListener l); + void removePropertyChangeListener(PropertyChangeListener listener); + + PropertyChangeListener[] getPropertyChangeListeners(); + + void addPropertyChangeListener(String propertyName, PropertyChangeListener listener); + + void removePropertyChangeListener(String propertyName, PropertyChangeListener listener); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsListener.java b/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsListener.java deleted file mode 100644 index c760305073a..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsListener.java +++ /dev/null @@ -1,19 +0,0 @@ -package de.uka.ilkd.key.settings; - -import java.util.EventObject; - - - -/** - * This interface is implemented by objects that listen to settings object. An object implementing - * the settings interface will call the method settingChanged of the listener - */ -public interface SettingsListener { - - /** - * called by the Settings object to inform the listener that its state has changed - * - * @param e the Event sent to the listener - */ - void settingsChanged(EventObject e); -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java index 46952c25bac..5a6b2ea5abc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java @@ -1,7 +1,5 @@ package de.uka.ilkd.key.settings; -import java.util.EventObject; -import java.util.LinkedList; import java.util.Objects; import java.util.Properties; @@ -18,21 +16,25 @@ import org.slf4j.LoggerFactory; -public class StrategySettings implements Settings, Cloneable { +public class StrategySettings extends AbstractSettings { public static final Logger LOGGER = LoggerFactory.getLogger(StrategySettings.class); - private static final String STRATEGY_KEY = "[Strategy]ActiveStrategy"; - private static final String STEPS_KEY = "[Strategy]MaximumNumberOfAutomaticApplications"; - private static final String TIMEOUT_KEY = "[Strategy]Timeout"; + public static final String STRATEGY_KEY = "[Strategy]ActiveStrategy"; + public static final String STEPS_KEY = "[Strategy]MaximumNumberOfAutomaticApplications"; + public static final String TIMEOUT_KEY = "[Strategy]Timeout"; + private static final String PROP_STRATEGY_PROPERTIES = "strategyProperties"; - private final LinkedList listenerList = new LinkedList<>(); private Name activeStrategy; - /** maximal number of automatic rule applications before an interaction is required */ + /** + * maximal number of automatic rule applications before an interaction is required + */ private int maxSteps = -1; - /** maximal time in ms after which automatic rule application is aborted */ + /** + * maximal time in ms after which automatic rule application is aborted + */ private long timeout = -1; private StrategyProperties strategyProperties = new StrategyProperties(); @@ -65,10 +67,9 @@ public int getMaxSteps() { * @param mSteps maximal amount of heuristic steps */ public void setMaxSteps(int mSteps) { - if (maxSteps != mSteps) { - maxSteps = mSteps; - fireSettingsChanged(); - } + var old = maxSteps; + maxSteps = mSteps; + firePropertyChange(STEPS_KEY, old, maxSteps); } /** @@ -86,10 +87,9 @@ public Name getStrategy() { * @param name */ public void setStrategy(Name name) { - if (!name.equals(activeStrategy)) { - activeStrategy = name; - fireSettingsChanged(); - } + var old = this.activeStrategy; + activeStrategy = name; + firePropertyChange(STRATEGY_KEY, old, activeStrategy); } /* @@ -132,13 +132,19 @@ public void readSettings(Properties props) { } // set strategy options - strategyProperties = StrategyProperties.read(props); + setStrategyProperties(StrategyProperties.read(props)); // set max steps - maxSteps = numSteps; + setMaxSteps(numSteps); // set time out - this.timeout = localTimeout; + setTimeout(localTimeout); + } + + private void setStrategyProperties(StrategyProperties props) { + var old = strategyProperties; + strategyProperties = props; + firePropertyChange(PROP_STRATEGY_PROPERTIES, old, strategyProperties); } /* @@ -148,9 +154,10 @@ public void readSettings(Properties props) { */ public void writeSettings(Properties props) { if (getStrategy() == null) { - // It would be bedder to return the name of the default factory defined by the profile + // It would be better to return the name of the default factory defined by the profile // used by the proof - // in which this strategysettings is used or just not to save the strategy because it is + // in which this strategy settings is used or just not to save the strategy because it + // is // not defined. setStrategy(JavaCardDLStrategyFactory.NAME); } @@ -164,29 +171,6 @@ public void writeSettings(Properties props) { strategyProperties.write(props); } - /** - * sends the message that the state of this setting has been changed to its registered listeners - * (not thread-safe) - */ - protected void fireSettingsChanged() { - for (SettingsListener aListenerList : listenerList) { - aListenerList.settingsChanged(new EventObject(this)); - } - } - - /** - * adds a listener to the settings object - * - * @param l the listener - */ - public void addSettingsListener(SettingsListener l) { - listenerList.add(l); - } - - public void removeSettingsListener(SettingsListener l) { - listenerList.remove(l); - } - /** * returns a shallow copy of the strategy properties */ @@ -198,10 +182,9 @@ public StrategyProperties getActiveStrategyProperties() { * sets the strategy properties if different from current ones */ public void setActiveStrategyProperties(StrategyProperties p) { - if (!p.equals(strategyProperties)) { - this.strategyProperties = (StrategyProperties) p.clone(); - fireSettingsChanged(); - } + var old = this.strategyProperties; + this.strategyProperties = (StrategyProperties) p.clone(); + firePropertyChange(PROP_STRATEGY_PROPERTIES, old, this.strategyProperties); } /** @@ -220,10 +203,9 @@ public long getTimeout() { * @param timeout a long specifying the timeout in ms */ public void setTimeout(long timeout) { - if (timeout != this.timeout) { - this.timeout = timeout; - fireSettingsChanged(); - } + var old = this.timeout; + this.timeout = timeout; + firePropertyChange(TIMEOUT_KEY, old, timeout); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java index d021bd4d8e3..64316f73e40 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java @@ -1,7 +1,5 @@ package de.uka.ilkd.key.settings; -import java.util.EventObject; -import java.util.LinkedList; import java.util.Properties; import de.uka.ilkd.key.logic.label.OriginTermLabel; @@ -15,25 +13,19 @@ * * @author lanzinger */ -public class TermLabelSettings implements Settings, Cloneable { +public class TermLabelSettings extends AbstractSettings { private static final Logger LOGGER = LoggerFactory.getLogger(TermLabelSettings.class); /** * Property key for {@link #getUseOriginLabels()} */ - private static final String USE_ORIGIN_LABELS = "[Labels]UseOriginLabels"; + public static final String USE_ORIGIN_LABELS = "[Labels]UseOriginLabels"; /** * @see {@link #getUseOriginLabels()} */ private boolean useOriginLabels = true; - /** - * @see #addSettingsListener(SettingsListener) - * @see #removeSettingsListener(SettingsListener) - */ - private final LinkedList listenerList = new LinkedList<>(); - @Override public void readSettings(Properties props) { String str = props.getProperty(USE_ORIGIN_LABELS); @@ -66,32 +58,8 @@ public boolean getUseOriginLabels() { * @param useOriginLabels whether {@link OriginTermLabel}s should be used. */ public void setUseOriginLabels(boolean useOriginLabels) { - if (this.useOriginLabels != useOriginLabels) { - this.useOriginLabels = useOriginLabels; - fireSettingsChanged(); - } - } - - @Override - public void addSettingsListener(SettingsListener l) { - listenerList.add(l); - } - - /** - * Removes a listener from this settings object. - * - * @param l the listener to remove. - */ - public void removeSettingsListener(SettingsListener l) { - listenerList.remove(l); - } - - /** - * Notify all listeners of the current state of this settings object. - */ - protected void fireSettingsChanged() { - for (SettingsListener aListenerList : listenerList) { - aListenerList.settingsChanged(new EventObject(this)); - } + var old = this.useOriginLabels; + this.useOriginLabels = useOriginLabels; + firePropertyChange(USE_ORIGIN_LABELS, old, useOriginLabels); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java index bcd23221601..17a20bb4786 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -71,7 +71,7 @@ public SLEnvInput(String javaPath, Profile profile) { public static String getLanguage() { GeneralSettings gs = ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); - if (gs.useJML()) { + if (gs.isUseJML()) { return "JML"; } else { return "no"; @@ -357,7 +357,7 @@ public ImmutableSet read() throws ProofInputException { final GeneralSettings gs = ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); - if (gs.useJML()) { + if (gs.isUseJML()) { return createSpecs(new JMLSpecExtractor(initConfig.getServices())); } else { return null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java b/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java index 7265079e4ca..898ccedf820 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java @@ -5,6 +5,7 @@ import java.io.File; import java.util.HashMap; +import java.util.Map; import java.util.Map.Entry; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -153,8 +154,9 @@ public static void setOneStepSimplificationEnabled(Proof proof, boolean enabled) * @throws ProblemLoaderException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public static HashMap setDefaultTacletOptions(File baseDir, - String javaPathInBaseDir) throws ProblemLoaderException, ProofInputException { + public static Map setDefaultTacletOptions(File baseDir, + String javaPathInBaseDir) + throws ProblemLoaderException, ProofInputException { if (!ProofSettings.isChoiceSettingInitialised()) { // Make sure that required files exists File javaFile = new File(baseDir, javaPathInBaseDir); @@ -189,9 +191,9 @@ public static HashMap setDefaultTacletOptions(File baseDir, * @throws ProblemLoaderException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public static HashMap setDefaultTacletOptionsForTarget(File javaFile, - String containerTypeName, final String targetName) - throws ProblemLoaderException, ProofInputException { + public static Map setDefaultTacletOptionsForTarget(File javaFile, + String containerTypeName, + final String targetName) throws ProblemLoaderException, ProofInputException { if (!ProofSettings.isChoiceSettingInitialised()) { KeYEnvironment environment = null; Proof proof = null; @@ -235,16 +237,16 @@ public static HashMap setDefaultTacletOptionsForTarget(File java * * @return The original settings which are overwritten. */ - public static HashMap setDefaultTacletOptions() { + public static Map setDefaultTacletOptions() { // Assert.assertTrue(ProofSettings.isChoiceSettingInitialised()); // Set default taclet options ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - HashMap oldSettings = choiceSettings.getDefaultChoices(); + var oldSettings = choiceSettings.getDefaultChoices(); HashMap newSettings = new HashMap<>(oldSettings); newSettings.putAll(MiscTools.getDefaultTacletOptions()); choiceSettings.setDefaultChoices(newSettings); // Make sure that default taclet options are set - HashMap updatedChoiceSettings = + var updatedChoiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); for (Entry entry : newSettings.entrySet()) { // Assert.assertEquals(entry.getValue(), updatedChoiceSettings.get(entry.getKey())); @@ -257,12 +259,12 @@ public static HashMap setDefaultTacletOptions() { * * @param options The taclet options to restore. */ - public static void restoreTacletOptions(HashMap options) { + public static void restoreTacletOptions(Map options) { if (options != null) { // Assert.assertTrue(ProofSettings.isChoiceSettingInitialised()); ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(options); // Make sure that taclet options are restored - HashMap updatedChoiceSettings = + var updatedChoiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); for (Entry entry : options.entrySet()) { // Assert.assertEquals(entry.getValue(), updatedChoiceSettings.get(entry.getKey())); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index 04458b9594f..8e53ecd37f9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java @@ -79,13 +79,13 @@ public boolean useUninterpretedMultiplicationIfNecessary() { @Override public long getMaximumInteger() { - return ProofDependentSMTSettings.getDefaultSettingsData().maxInteger; + return ProofDependentSMTSettings.getDefaultSettingsData().getMaxInteger(); } @Override public long getMinimumInteger() { - return ProofDependentSMTSettings.getDefaultSettingsData().minInteger; + return ProofDependentSMTSettings.getDefaultSettingsData().getMinInteger(); } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 82b3b14afba..48eeb0a3259 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1,10 +1,13 @@ package de.uka.ilkd.key.gui; import java.awt.*; +import java.awt.event.*; import java.awt.event.ActionEvent; import java.awt.event.KeyEvent; import java.awt.event.KeyListener; import java.awt.event.MouseEvent; +import java.beans.PropertyChangeEvent; +import java.beans.PropertyChangeListener; import java.io.File; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; @@ -53,7 +56,6 @@ import de.uka.ilkd.key.proof.ProofEvent; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.smt.SolverTypeCollection; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; @@ -485,7 +487,7 @@ private void layoutMain() { // FIXME do this NOT in layout of GUI // minimize interaction final boolean stupidMode = - ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().tacletFilter(); + ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().getTacletFilter(); userInterface.getProofControl().setMinimizeInteraction(stupidMode); // set up actions @@ -1086,7 +1088,7 @@ private JMenuItem setupSpeclangMenu() { GeneralSettings gs = ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); JRadioButtonMenuItem jmlButton = - new JRadioButtonMenuItem("Source File Comments Are JML", gs.useJML()); + new JRadioButtonMenuItem("Source File Comments Are JML", gs.isUseJML()); result.add(jmlButton); group.add(jmlButton); jmlButton.setIcon(IconFactory.jmlLogo(15)); @@ -1096,7 +1098,7 @@ private JMenuItem setupSpeclangMenu() { }); JRadioButtonMenuItem noneButton = - new JRadioButtonMenuItem("Source File Comments Are Ignored", !gs.useJML()); + new JRadioButtonMenuItem("Source File Comments Are Ignored", !gs.isUseJML()); result.add(noneButton); group.add(noneButton); noneButton.addActionListener(e -> { @@ -1647,7 +1649,8 @@ public void shutDown(EventObject e) { } - class MainProofListener implements AutoModeListener, KeYSelectionListener, SettingsListener { + class MainProofListener + implements AutoModeListener, KeYSelectionListener, PropertyChangeListener { Proof proof = null; @@ -1670,11 +1673,11 @@ public synchronized void selectedProofChanged(KeYSelectionEvent e) { LOGGER.debug("Main: initialize with new proof"); if (proof != null && !proof.isDisposed()) { - proof.getSettings().getStrategySettings().removeSettingsListener(this); + proof.getSettings().getStrategySettings().removePropertyChangeListener(this); } proof = e.getSource().getSelectedProof(); if (proof != null) { - proof.getSettings().getStrategySettings().addSettingsListener(this); + proof.getSettings().getStrategySettings().removePropertyChangeListener(this); } disableCurrentGoalView = false; @@ -1707,12 +1710,9 @@ public synchronized void autoModeStopped(ProofEvent e) { getMediator().addKeYSelectionListenerChecked(proofListener); } - /** - * invoked when the strategy of a proof has been changed - */ @Override - public synchronized void settingsChanged(EventObject e) { - if (proof.getSettings().getStrategySettings() == e.getSource()) { + public synchronized void propertyChange(PropertyChangeEvent evt) { + if (proof.getSettings().getStrategySettings() == evt.getSource()) { // updateAutoModeConfigButton(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java index c5ab032df8e..53e3e09cafd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java @@ -1,6 +1,7 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import javax.swing.*; import de.uka.ilkd.key.core.KeYSelectionEvent; @@ -9,7 +10,6 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.settings.ViewSettings; public class HeatmapToggleAction extends MainWindowAction { @@ -34,8 +34,8 @@ public HeatmapToggleAction(MainWindow mainWindow) { ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); setSelected(vs.isShowHeatmap()); - final SettingsListener setListener = e -> setSelected(vs.isShowHeatmap()); - vs.addSettingsListener(setListener); + final PropertyChangeListener setListener = e -> setSelected(vs.isShowHeatmap()); + vs.addPropertyChangeListener(setListener); final KeYSelectionListener selListener = new KeYSelectionListener() { @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java index bdd0a7cdd8b..b1f02b872ca 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java @@ -1,13 +1,13 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import java.util.EventObject; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; public final class HidePackagePrefixToggleAction extends MainWindowAction { public static final String NAME = "Hide Package Prefix"; @@ -23,16 +23,17 @@ public final class HidePackagePrefixToggleAction extends MainWindowAction { * Such changes can occur in the Eclipse context when settings are changed in for instance the * KeYIDE. */ - private final SettingsListener viewSettingsListener = this::handleViewSettingsChanged; + private final PropertyChangeListener viewSettingsListener = this::handleViewSettingsChanged; public HidePackagePrefixToggleAction(MainWindow mainWindow) { super(mainWindow); setName(NAME); setTooltip(TOOL_TIP); + // Attention: The listener is never + // removed, because there is only one + // MainWindow! ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(viewSettingsListener); // Attention: The listener is never - // removed, because there is only one - // MainWindow! + .addPropertyChangeListener(viewSettingsListener); updateSelectedState(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java index 419ae089be6..0e01a646914 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java @@ -1,10 +1,11 @@ package de.uka.ilkd.key.gui.actions; + +import java.beans.PropertyChangeListener; import java.util.EventObject; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; /* * Is this a legacy option? Finding instantiations seems to be done by the prover, even if this @@ -29,22 +30,24 @@ public class MinimizeInteraction extends KeYMenuCheckBox { * Such changes can occur in the Eclipse context when settings are changed in for instance the * KeYIDE. */ - private final SettingsListener generalSettingsListener = this::handleGeneralSettingsChanged; + private final PropertyChangeListener generalSettingsListener = + this::handleGeneralSettingsChanged; public MinimizeInteraction(MainWindow mainWindow) { super(mainWindow, NAME); this.mainWindow = mainWindow; setName("MinimizeInteractionInstance"); setTooltip(TOOL_TIP); + // Attention: The listener is never// removed, because there is only one + // MainWindow! ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings() - .addSettingsListener(generalSettingsListener); // Attention: The listener is never - // removed, because there is only one - // MainWindow! + .addPropertyChangeListener(generalSettingsListener); updateSelectedState(); } protected void updateSelectedState() { - setSelected(ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().tacletFilter()); + setSelected( + ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().getTacletFilter()); } @Override @@ -62,7 +65,7 @@ protected void updateMainWindow(boolean b) { protected void handleGeneralSettingsChanged(EventObject e) { updateSelectedState(); final boolean tacletFilter = - ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().tacletFilter(); + ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().getTacletFilter(); updateMainWindow(tacletFilter); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java index 426da91dabb..09445f5badb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java @@ -1,13 +1,15 @@ package de.uka.ilkd.key.gui.actions; + import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import java.util.EventObject; import javax.swing.*; +import javax.swing.JCheckBoxMenuItem; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; public class PrettyPrintToggleAction extends MainWindowAction { public static final String NAME = "Use Pretty Syntax"; @@ -25,16 +27,17 @@ public class PrettyPrintToggleAction extends MainWindowAction { * Such changes can occur in the Eclipse context when settings are changed in for instance the * KeYIDE. */ - private final SettingsListener viewSettingsListener = this::handleViewSettingsChanged; + private final PropertyChangeListener viewSettingsListener = this::handleViewSettingsChanged; public PrettyPrintToggleAction(MainWindow mainWindow) { super(mainWindow); setName(NAME); setTooltip(TOOL_TIP); + // Attention: The listener is never + // removed, because there is only one + // MainWindow! ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(viewSettingsListener); // Attention: The listener is never - // removed, because there is only one - // MainWindow! + .addPropertyChangeListener(viewSettingsListener); updateSelectedState(); } @@ -49,9 +52,9 @@ protected void updateSelectedState() { @Override public void actionPerformed(ActionEvent e) { boolean selected = ((JCheckBoxMenuItem) e.getSource()).isSelected(); - NotationInfo.DEFAULT_PRETTY_SYNTAX = selected; // Needs to be executed before the - // ViewSettings are modified, because the UI - // will react on the settings change event! + // Needs to be executed before the// ViewSettings are modified, because the UI + // will react on the settings change event! + NotationInfo.DEFAULT_PRETTY_SYNTAX = selected; ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setUsePretty(selected); updateMainWindow(selected); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java index adc6a4aad20..c04634f9559 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java @@ -34,7 +34,7 @@ public SaveBundleAction(MainWindow mainWindow) { // react to setting changes GeneralSettings settings = ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); - settings.addSettingsListener(e -> updateStatus()); + settings.addPropertyChangeListener(e -> updateStatus()); // react to changes of proof selection mainWindow.getMediator().addKeYSelectionListener(new KeYSelectionListener() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSequentViewTooltipAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSequentViewTooltipAction.java index 916d24530fe..cd3b68e44ab 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSequentViewTooltipAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSequentViewTooltipAction.java @@ -1,12 +1,13 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import javax.swing.*; +import javax.swing.JCheckBoxMenuItem; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.nodeviews.SequentView; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.settings.ViewSettings; /** @@ -28,7 +29,7 @@ public class ToggleSequentViewTooltipAction extends MainWindowAction { private static final long serialVersionUID = -3352122484627890921L; /** Listens to changes to the view settings to call {@link #updateSelectedState()}. */ - private final SettingsListener viewSettingsListener = e -> updateSelectedState(); + private final PropertyChangeListener viewSettingsListener = e -> updateSelectedState(); /** * Crate a new action. @@ -40,7 +41,7 @@ public ToggleSequentViewTooltipAction(MainWindow mainWindow) { setName(NAME); setTooltip(TOOL_TIP); ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(viewSettingsListener); + .addPropertyChangeListener(viewSettingsListener); updateSelectedState(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSourceViewTooltipAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSourceViewTooltipAction.java index bd409b41be4..101efd64c0b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSourceViewTooltipAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSourceViewTooltipAction.java @@ -1,11 +1,11 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.settings.ViewSettings; /** @@ -26,7 +26,7 @@ public class ToggleSourceViewTooltipAction extends MainWindowAction { // private static final long serialVersionUID = -3352122484627890921L; /** Listens to changes to the view settings to call {@link #updateSelectedState()}. */ - private final SettingsListener viewSettingsListener = e -> updateSelectedState(); + private final PropertyChangeListener viewSettingsListener = e -> updateSelectedState(); /** * Create a new action. @@ -38,7 +38,7 @@ public ToggleSourceViewTooltipAction(MainWindow mainWindow) { setName(NAME); setTooltip(TOOL_TIP); ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(viewSettingsListener); + .addPropertyChangeListener(viewSettingsListener); updateSelectedState(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java index 5cce73de7de..205389a2996 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java @@ -1,13 +1,14 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; import java.util.EventObject; import javax.swing.*; +import javax.swing.JCheckBoxMenuItem; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.SettingsListener; import de.uka.ilkd.key.util.UnicodeHelper; public class UnicodeToggleAction extends MainWindowAction { @@ -26,16 +27,16 @@ public class UnicodeToggleAction extends MainWindowAction { * Such changes can occur in the Eclipse context when settings are changed in for instance the * KeYIDE. */ - private final SettingsListener viewSettingsListener = this::handleViewSettingsChanged; + private final PropertyChangeListener viewSettingsListener = this::handleViewSettingsChanged; public UnicodeToggleAction(MainWindow window) { super(window); setName(NAME); setTooltip(TOOL_TIP); + // Attention: The listener is never// removed, because there is only one + // MainWindow! ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(viewSettingsListener); // Attention: The listener is never - // removed, because there is only one - // MainWindow! + .addPropertyChangeListener(viewSettingsListener); updateSelectedState(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java index 07f6af54917..4d645dc9763 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java @@ -131,10 +131,11 @@ public String value() { @Override public void parseFrom(String v) { - if (!Objects.equals(value(), v)) { + final var old = value(); + if (!Objects.equals(old, v)) { currentValue = fromHex(v); properties.setProperty(getKey(), v); - fireSettingsChange(); + firePropertyChange(getKey(), old, currentValue); } } @@ -146,9 +147,10 @@ public String getKey() { @Override public void set(Color value) { if (currentValue != value) { + var old = currentValue; currentValue = value; properties.setProperty(getKey(), toHex(value)); - fireSettingsChange(); + firePropertyChange(getKey(), old, value); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/ChoiceSelector.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/ChoiceSelector.java index 43e832ca7ce..ff7e0dff073 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/ChoiceSelector.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/ChoiceSelector.java @@ -1,11 +1,24 @@ package de.uka.ilkd.key.gui.configuration; import java.awt.*; +import java.awt.BorderLayout; +import java.awt.Dimension; import java.io.FileNotFoundException; import java.io.IOException; import java.io.InputStream; import java.util.*; import javax.swing.*; +import javax.swing.BorderFactory; +import javax.swing.JButton; +import javax.swing.JDialog; +import javax.swing.JFrame; +import javax.swing.JList; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JTextArea; +import javax.swing.ListSelectionModel; +import javax.swing.ScrollPaneConstants; import javax.swing.border.TitledBorder; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -23,8 +36,8 @@ public class ChoiceSelector extends JDialog { private static final String EXPLANATIONS_RESOURCE = "/de/uka/ilkd/key/gui/help/choiceExplanations.xml"; private final ChoiceSettings settings; - private final HashMap category2DefaultChoice; - private HashMap> category2Choices; + private final Map category2DefaultChoice; + private Map> category2Choices; private boolean changed = false; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index 03469a5b10c..28cae1990bd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -161,10 +161,10 @@ public void readSettings(Properties props) { } void setKeyStroke(String key, KeyStroke stroke, boolean override) { - boolean exists = properties.contains(key); - if (override || !exists) { + var old = getKeyStroke(key, null); + if (override || (old == null)) { properties.setProperty(key, stroke != null ? stroke.toString() : ""); - fireSettingsChange(); + firePropertyChange(key, old, stroke); } } @@ -174,13 +174,13 @@ KeyStroke getKeyStroke(String key, KeyStroke defaultValue) { if (ks != null) { return ks; } - } catch (Exception e) { + } catch (Exception ignored) { } return defaultValue; } public void save() { - LOGGER.info("Save keyboard shortcuts to: " + SETTINGS_FILE.getAbsolutePath()); + LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.getAbsolutePath()); SETTINGS_FILE.getParentFile().mkdirs(); try (Writer writer = new FileWriter(SETTINGS_FILE, StandardCharsets.UTF_8)) { properties.store(writer, "KeY's KeyStrokes"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java index 733b05faabc..5db279d60ca 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java @@ -207,7 +207,7 @@ private JCheckBox getLemmaCheckBox() { changedToNotSelected(); lemmaCheckbox.setSelected(false); ProofIndependentSettings.DEFAULT_INSTANCE.getLemmaGeneratorSettings() - .showDialogUsingAxioms( + .setShowDialogUsingAxioms( showDialogUsingAxioms && infoDialog.showThisDialogNextTime()); } } else { @@ -316,7 +316,7 @@ private JButton getAddAxiomFileButton() { firstTimeAddingAxioms = !infoDialog.showDialog(INFO_TEXT, LoadUserTacletsDialog.this); ProofIndependentSettings.DEFAULT_INSTANCE.getLemmaGeneratorSettings() - .showDialogAddingAxioms(infoDialog.showThisDialogNextTime()); + .setShowDialogAddingAxioms(infoDialog.showThisDialogNextTime()); if (firstTimeAddingAxioms) { return; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java index 113ee23c6dc..e024b2385ac 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java @@ -142,7 +142,7 @@ private void initClutterRules() { ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); clutterRuleSets = vs.getClutterRuleSets(); clutterRules = vs.getClutterRules(); - vs.addSettingsListener(e -> { + vs.addPropertyChangeListener(e -> { clutterRuleSets = vs.getClutterRuleSets(); clutterRules = vs.getClutterRules(); }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java index 5691a4d2f9d..c84af27393f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java @@ -36,7 +36,7 @@ public ShowOriginAction(PosInSequent pos) { setName("Show origin"); setEnabled(settings.getUseOriginLabels()); - settings.addSettingsListener(event -> setEnabled(settings.getUseOriginLabels())); + settings.addPropertyChangeListener(event -> setEnabled(settings.getUseOriginLabels())); setMenuPath("View"); lookupAcceleratorKey(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java index a5d5e6e8792..e062a1e1406 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java @@ -35,13 +35,13 @@ public ToggleOriginHighlightAction(MainWindow mainWindow) { + "highlight its origin in the source view."); putValue(KeyAction.CHECKBOX, true); - ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings() - .addSettingsListener(event -> { - boolean useOriginLabels = ProofIndependentSettings.DEFAULT_INSTANCE - .getTermLabelSettings().getUseOriginLabels(); + ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().addPropertyChangeListener( + event -> { + boolean useOriginLabels = ProofIndependentSettings.DEFAULT_INSTANCE + .getTermLabelSettings().getUseOriginLabels(); - setEnabled(useOriginLabels); - }); + setEnabled(useOriginLabels); + }); } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java index 9f09a54831b..2b33ce013de 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java @@ -149,7 +149,7 @@ public JComponent getPanel(MainWindow window) { chkRightClickMacros.setSelected(generalSettings.isRightClickMacro()); chkConfirmExit.setSelected(vs.confirmExit()); spAutoSaveProof.setValue(generalSettings.autoSavePeriod()); - chkMinimizeInteraction.setSelected(generalSettings.tacletFilter()); + chkMinimizeInteraction.setSelected(generalSettings.getTacletFilter()); spFontSizeTreeSequent.setSelectedIndex(vs.sizeIndex()); return this; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index f45a2d43ca1..133f2cdf083 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -295,8 +295,8 @@ public JComponent getPanel(MainWindow window) { private void setChoiceSettings(ChoiceSettings choiceSettings) { this.settings = choiceSettings; - category2Choice = settings.getDefaultChoices(); - category2Choices = settings.getChoices(); + category2Choice = new HashMap<>(settings.getDefaultChoices()); + category2Choices = new HashMap<>(settings.getChoices()); layoutChoiceSelector(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/TacletTranslationSelection.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/TacletTranslationSelection.java index 0f5ed32d579..e69de29bb2d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/TacletTranslationSelection.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/TacletTranslationSelection.java @@ -1,263 +0,0 @@ -package de.uka.ilkd.key.gui.smt; - -import java.awt.*; -import java.awt.event.MouseAdapter; -import java.awt.event.MouseEvent; -import java.util.Set; -import javax.swing.*; -import javax.swing.tree.TreeNode; - -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.proof.TacletIndex; -import de.uka.ilkd.key.rule.NoPosTacletApp; -import de.uka.ilkd.key.settings.DefaultSMTSettings; -import de.uka.ilkd.key.taclettranslation.assumptions.SupportedTaclets; -import de.uka.ilkd.key.taclettranslation.assumptions.SupportedTaclets.TreeItem; -import de.uka.ilkd.key.taclettranslation.assumptions.SupportedTaclets.TreeItem.SelectionMode; - - -abstract class TreePanel extends JPanel { - - private static final long serialVersionUID = 1L; - protected TreeNode root; - protected JTree tree; - - protected void addComponent(JComponent comp) { - comp.setBackground(UIManager.getColor("Tree.textBackground")); - comp.setFont(UIManager.getFont("Tree.font")); - this.add(comp); - } - - - - public int getHeight() { - return this.getPreferredSize().height; - } - - protected void newMode(TreeItem node, SelectionMode mode, SupportedTaclets supportedTaclets) { - - node.setMode(mode); - - propergateToRoot(node, SelectionMode.user); - - supportedTaclets.validateSelectionModes(); - - tree.validate(); - tree.repaint(); - - } - - protected abstract JPanel init(TreeItem node, TreeItem rootNode, JTree t, - DefaultSMTSettings settings); - - protected void propergateToRoot(TreeItem node, SelectionMode mode) { - TreeItem parent = (TreeItem) node.getParent(); - if (parent != null) { - - parent.setMode(mode); - propergateToRoot(parent, mode); - } - } - - protected void propergateToChild(TreeItem node, SelectionMode mode) { - - for (int i = 0; i < node.getChildCount(); i++) { - TreeItem child = (TreeItem) node.getChildAt(i); - propergateToChild(child, mode); - child.setMode(mode); - } - } - -} - - -class InnerPanel extends TreePanel { - - private static final long serialVersionUID = 1L; - private final JLabel title = new JLabel(); - private final JRadioButton radioAll = new JRadioButton("all"); - private final JRadioButton radioNothing = new JRadioButton("none"); - private final JRadioButton radioUser = new JRadioButton("custom"); - private TreeItem currentNode = null; - private final ButtonGroup buttonGroup = new ButtonGroup(); - - public InnerPanel(final SupportedTaclets supportedTaclets) { - this.setBackground(UIManager.getColor("Tree.textBackground")); - // this.setLayout(new BoxLayout(this, BoxLayout.X_AXIS)); - - addComponent(title); - addComponent(radioAll); - addComponent(radioNothing); - addComponent(radioUser); - - radioUser.setEnabled(false); - - ToolTipManager.sharedInstance().registerComponent(title); - - buttonGroup.add(radioAll); - buttonGroup.add(radioNothing); - buttonGroup.add(radioUser); - radioNothing.setSelected(true); - - radioAll.addActionListener(e -> { - propergateToChild(currentNode, SelectionMode.all); - newMode(currentNode, SelectionMode.all, supportedTaclets); - - }); - - radioNothing.addActionListener(e -> { - propergateToChild(currentNode, SelectionMode.nothing); - newMode(currentNode, SelectionMode.nothing, supportedTaclets); - - }); - } - - @Override - protected JPanel init(TreeItem node, TreeItem rootNode, JTree t, DefaultSMTSettings settings) { - - currentNode = node; - root = rootNode; - this.tree = t; - title.setText(currentNode.toString() + ": "); - - - switch (currentNode.getMode()) { - case all: - radioAll.setSelected(true); - - break; - case nothing: - radioNothing.setSelected(true); - - break; - - case user: - radioAll.setSelected(false); - radioNothing.setSelected(false); - radioUser.setSelected(true); - - break; - } - - return this; - - } -} - - -class LeafPanel extends TreePanel { - - private static TacletIndex index; - private static final SelectionListener listener = new SelectionListener(); - private static final long serialVersionUID = 1L; - private TreeItem currentNode = null; - private final JCheckBox tacletName = new JCheckBox(); - private final JLabel infoButton = new JLabel("info"); - private final JLabel genericLabel = new JLabel(); - - public static KeYSelectionListener getSelectionListener() { - return listener; - } - - private static class SelectionListener implements KeYSelectionListener { - - /** focused node has changed */ - public void selectedNodeChanged(KeYSelectionEvent e) { - react(e); - } - - private void react(KeYSelectionEvent e) { - if (e.getSource().getSelectedProof() != null - && e.getSource().getSelectedGoal() != null) { - index = e.getSource().getSelectedGoal().indexOfTaclets(); - } else { - index = null; - } - } - - /** - * the selected proof has changed (e.g. a new proof has been loaded) - */ - public void selectedProofChanged(KeYSelectionEvent e) { - react(e); - } - - } - - public LeafPanel(final SupportedTaclets supportedTaclets) { - this.setBackground(UIManager.getColor("Tree.textBackground")); - addComponent(tacletName); - addComponent(infoButton); - addComponent(genericLabel); - ToolTipManager.sharedInstance().registerComponent(tacletName); - infoButton.setForeground(Color.BLUE); - - tacletName.addActionListener(event -> { - newMode(currentNode, - tacletName.isSelected() ? SelectionMode.all : SelectionMode.nothing, - supportedTaclets); - // selected(title.isSelected()); - tree.repaint(); - - }); - infoButton.addMouseListener(new MouseAdapter() { - - @Override - public void mouseClicked(MouseEvent e) { - - showInfo(currentNode); - super.mouseClicked(e); - } - }); - - } - - private void showInfo(TreeItem item) { - if (index == null) { - JOptionPane.showMessageDialog(this, - "You must load a proof to make the" + " information for this taclet available.", - "Taclet View", JOptionPane.CLOSED_OPTION); - return; - } - final Set apps = index.allNoPosTacletApps(); - for (final NoPosTacletApp app : apps) { - if (app.taclet().name().toString().equals(item.toString())) { - // TODO uncomment - // TacletView.getInstance().showTacletView(app.taclet(), - // true); - break; - } - - } - - } - - @Override - protected JPanel init(TreeItem node, TreeItem r, JTree t, DefaultSMTSettings smtSettings) { - - int max = smtSettings != null ? smtSettings.getMaxNumberOfGenerics() : 0; - currentNode = node; - this.tree = t; - this.root = r; - tacletName.setText(node.toString()); - tacletName.setSelected(node.getMode() == SelectionMode.all); - int count = node.getGenericCount(); - if (count > 0) { - genericLabel.setVisible(true); - if (max < count) { - genericLabel.setForeground(Color.RED); - genericLabel.setText("too many generic sorts: " + count); - } else { - genericLabel.setForeground(Color.GREEN); - genericLabel.setText("generic sorts: " + count); - } - - } else { - genericLabel.setVisible(false); - } - - return this; - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java index d75e83737e9..b0af64d17f0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java @@ -112,7 +112,6 @@ public JComponent getPanel(MainWindow window) { public void applySettings(MainWindow window) { ProofIndependentSMTSettings pi = SettingsManager.getSmtPiSettings(); pi.copy(settings); - pi.fireSettingsChanged(); setSmtSettings(pi.clone()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java index e45a20148b8..20039998df7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java @@ -57,7 +57,7 @@ public String getDescription() { public JComponent getPanel(MainWindow window) { ProofDependentSMTSettings pdSettings = SettingsManager.getSmtPdSettings(window).clone(); ProofIndependentSMTSettings piSettings = SettingsManager.getSmtPiSettings().clone(); - maxNumberOfGenerics.setValue(pdSettings.maxGenericSorts); + maxNumberOfGenerics.setValue(pdSettings.getMaxGenericSorts()); fileChooserPanel.setText(piSettings.getPathForTacletTranslation()); // fileChooserPanel.setEnabled(piSettings.storeTacletTranslationToFile); return this; @@ -68,11 +68,8 @@ public void applySettings(MainWindow window) { ProofDependentSMTSettings currentPd = SettingsManager.getSmtPdSettings(window); ProofIndependentSMTSettings currentPi = SettingsManager.getSmtPiSettings(); - currentPd.maxGenericSorts = (Integer) maxNumberOfGenerics.getValue(); + currentPd.setMaxGenericSorts((Integer) maxNumberOfGenerics.getValue()); currentPi.setPathForTacletTranslation(fileChooserPanel.getText()); currentPi.setStoreTacletTranslationToFile(!fileChooserPanel.getText().trim().isEmpty()); - - currentPd.fireSettingsChanged(); - currentPi.fireSettingsChanged(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java index 5be146cc8b1..114d5c797f5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java @@ -90,62 +90,65 @@ public void setSmtSettings(ProofDependentSMTSettings settings) { setEnabled(false); } else { setEnabled(true); - useExplicitTypeHierachy.setSelected(settings.useExplicitTypeHierarchy); - useNullInstantiation.setSelected(settings.useNullInstantiation); - useBuiltInUniqueness.setSelected(settings.useBuiltInUniqueness); - useConstantsForIntegers.setSelected(settings.useConstantsForIntegers); - minField.setValue(settings.minInteger); - maxField.setValue(settings.maxInteger); + useExplicitTypeHierachy.setSelected(settings.isUseExplicitTypeHierarchy()); + useNullInstantiation.setSelected(settings.isUseNullInstantiation()); + useBuiltInUniqueness.setSelected(settings.isUseBuiltInUniqueness()); + useConstantsForIntegers.setSelected(settings.isUseConstantsForIntegers()); + minField.setValue(settings.getMinInteger()); + maxField.setValue(settings.getMaxInteger()); } } protected JCheckBox createUseExplicitTypeHierachy() { return addCheckBox("Use an explicit type hierarchy.", infoUseExplicitTypeHierarchy, false, - e -> settings.useExplicitTypeHierarchy = useExplicitTypeHierachy.isSelected()); + e -> settings.setUseExplicitTypeHierarchy(useExplicitTypeHierachy.isSelected())); } protected JCheckBox createNullInstantiation() { return addCheckBox("Instantiate hierarchy assumptions if possible (recommended).", infoUseNullInstantiation, false, - e -> settings.useNullInstantiation = useNullInstantiation.isSelected()); + e -> settings.setUseNullInstantiation(useNullInstantiation.isSelected())); } protected JCheckBox createBuiltInUniqueness() { return addCheckBox("Use built-in mechanism for uniqueness if possible.", infoUseBuiltInUniqueness, false, - e -> settings.useBuiltInUniqueness = useBuiltInUniqueness.isSelected()); + e -> settings.setUseBuiltInUniqueness(useBuiltInUniqueness.isSelected())); } protected JCheckBox createUIMultiplication() { return addCheckBox("Use uninterpreted multiplication if necessary.", infoUseUIMultiplication, false, - e -> settings.useUIMultiplication = useUIMultiplication.isSelected()); + e -> settings.setUseUIMultiplication(useUIMultiplication.isSelected())); } protected JSpinner createMaxField() { JSpinner max = addNumberField("Maximum", Integer.MIN_VALUE, Integer.MAX_VALUE, 1, "", e -> { + long result = Integer.MAX_VALUE; if (settings != null) { - settings.maxInteger = e.longValue(); + result = settings.getMaxInteger(); } + try { + result = (long) maxField.getValue(); + maxField.setForeground(Color.BLACK); + } catch (Throwable ex) { + maxField.setForeground(Color.RED); + } + settings.setMaxInteger(result); }); - try { - max.setValue((long) Integer.MAX_VALUE); - max.setForeground(Color.BLACK); - } catch (IllegalArgumentException e) { - max.setForeground(Color.RED); - } + max.setValue(Integer.MAX_VALUE); return max; } protected JSpinner createMinField() { return addNumberField("Minimum", Integer.MIN_VALUE, Integer.MAX_VALUE, 1, "", - val -> settings.minInteger = val.longValue()); + val -> settings.setMinInteger(val.longValue())); } protected JCheckBox createConstantsForIntegers() { return addCheckBox("Active", infoUseConstantsForIntegers, false, e -> { - settings.useConstantsForIntegers = useConstantsForIntegers.isSelected(); + settings.setUseConstantsForIntegers(useConstantsForIntegers.isSelected()); maxField.setEnabled(useConstantsForIntegers.isSelected()); minField.setEnabled(useConstantsForIntegers.isSelected()); }); @@ -166,6 +169,5 @@ public JComponent getPanel(MainWindow window) { public void applySettings(MainWindow window) { ProofDependentSMTSettings current = SettingsManager.getSmtPdSettings(window); current.copy(settings);// transfer settings - current.fireSettingsChanged(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index 2f7899d3d57..f2e2118063b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -1,12 +1,12 @@ package de.uka.ilkd.key.gui.sourceview; import java.awt.Color; +import java.beans.PropertyChangeListener; import java.util.*; import java.util.regex.Pattern; import javax.swing.text.*; import de.uka.ilkd.key.gui.colors.ColorSettings; -import de.uka.ilkd.key.settings.SettingsListener; import static de.uka.ilkd.key.speclang.jml.JMLUtils.isJmlCommentStarter; @@ -251,7 +251,7 @@ private enum CommentState { /** * The settings listener of this document (registered in the static listener list). */ - private final transient SettingsListener listener = e -> updateStyles(); + private final transient PropertyChangeListener listener = e -> updateStyles(); /** * Creates a new JavaDocument and sets the syntax highlighting styles (as in eclipse default @@ -259,7 +259,7 @@ private enum CommentState { */ public JavaDocument() { updateStyles(); - ColorSettings.getInstance().addSettingsListener(listener); + ColorSettings.getInstance().addPropertyChangeListener(listener); // workaround for #1641: typing "enter" key shall insert only "\n", even on Windows putProperty(DefaultEditorKit.EndOfLineStringProperty, "\n"); @@ -272,7 +272,7 @@ public JavaDocument() { * Dispose this object. */ public void dispose() { - ColorSettings.getInstance().removeSettingsListener(listener); + ColorSettings.getInstance().removePropertyChangeListener(listener); } private void updateStyles() { diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ShowInteractiveBranchesAction.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ShowInteractiveBranchesAction.java index 58c85fec3af..7ccf201e660 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ShowInteractiveBranchesAction.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ShowInteractiveBranchesAction.java @@ -28,7 +28,7 @@ public ShowInteractiveBranchesAction(ExplorationModeModel model, MainWindow main model.addPropertyChangeListener(ExplorationModeModel.PROP_EXPLORE_MODE, e -> updateEnable()); ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addSettingsListener(e -> updateEnable()); + .addPropertyChangeListener(e -> updateEnable()); updateEnable(); } diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java index a38bf44264a..f47ad010619 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java @@ -84,14 +84,12 @@ private JSpinner getMaxProcesses() { return addNumberField("Concurrent processes:", 0, Integer.MAX_VALUE, 1, INFO_MAX_PROCESSES, obj -> { settings.setConcurrentProcesses(obj.intValue()); - settings.fireSettingsChanged(); }); } private JSpinner getMaxUnwinds() { return addNumberField("Maximal unwinds:", 0, Integer.MAX_VALUE, 1, INFO_MAX_UNWINDS, e -> { settings.setMaxUnwinds(e.intValue()); - settings.fireSettingsChanged(); }); } @@ -99,49 +97,42 @@ private JSpinner getMaxUnwinds() { private JTextField getSaveToFilePanel() { return addFileChooserPanel("Store test cases to folder:", "", INFO_SAVE_TO, true, e -> { settings.setOutputPath(saveToFilePanel.getText()); - settings.fireSettingsChanged(); }); } private JTextField getOpenJMLPanel() { return addFileChooserPanel("Location of openjml:", "", INFO_OPEN_JML_PATH, false, e -> { settings.setOpenjmlPath(openJMLPanel.getText()); - settings.fireSettingsChanged(); }); } private JTextField getObjenesisPanel() { return addFileChooserPanel("Location of objenesis:", "", INFO_OBJENESIS_PATH, false, e -> { settings.setObjenesisPath(objenesisPanel.getText()); - settings.fireSettingsChanged(); }); } private JCheckBox getJUnitPanel() { return addCheckBox("Generate JUnit and test oracle", INFO_USE_JUNIT, false, val -> { settings.setUseJunit(val); - settings.fireSettingsChanged(); }); } private JCheckBox getRemoveDuplicatesPanel() { return addCheckBox("Remove duplicates", INFO_REMOVE_DUPLICATES, false, val -> { settings.setRemoveDuplicates(val); - settings.fireSettingsChanged(); }); } private JCheckBox getRFLSelectionPanel() { return addCheckBox("Use reflection framework", INFO_RFL_SELECTION, false, val -> { settings.setRFL(val); - settings.fireSettingsChanged(); }); } private JCheckBox getSymbolicEx() { return addCheckBox("Apply symbolic execution", INFO_APPLY_SYMBOLIC_EX, false, val -> { settings.setApplySymbolicExecution(val); - settings.fireSettingsChanged(); }); } @@ -149,14 +140,12 @@ private JCheckBox getInvariantForall() { return addCheckBox("Require invariant for all objects", INFO_INVARIANT_FOR_ALL, false, val -> { settings.setInvariantForAll(val); - settings.fireSettingsChanged(); }); } private JCheckBox getIncludePostCondition() { return addCheckBox("Include post condition", INFO_INCLUDE_POSTCONDITION, false, val -> { settings.setIncludePostCondition(val); - settings.fireSettingsChanged(); }); } @@ -184,6 +173,5 @@ public JComponent getPanel(MainWindow window) { public void applySettings(MainWindow window) { TestGenerationSettings globalSettings = TestGenerationSettings.getInstance(); globalSettings.set(settings); - globalSettings.fireSettingsChanged(); } }