diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 5a8489b6123..00bd2641767 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -6,7 +6,7 @@ on: push: branches: - main - - 'releases/*' + - 'KeY-*' jobs: qodana: diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 1fb4812f631..ae93906d0fc 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -4,8 +4,9 @@ on: push: branches: [ "main" ] pull_request: - # The branches below must be a subset of the branches above - branches: [ "main" ] + branches: + - "main" + - "KeY-*" schedule: - cron: '21 21 * * 4' merge_group: diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index 3aea47e894d..756133f4889 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -6,7 +6,6 @@ on: jobs: doc: - # later limit to master only! runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index ef657be2e08..da6bf45f06b 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -5,7 +5,9 @@ on: push: branches: [ "main" ] pull_request: - branches: [ "main" ] + branches: + - "main" + - "KeY-*" merge_group: permissions: diff --git a/LICENSE.TXT b/LICENSE.TXT index 9ba1971ac0b..63eff5c638a 100644 --- a/LICENSE.TXT +++ b/LICENSE.TXT @@ -27,8 +27,8 @@ Sweden - WWW: http://key-project.org - e-mail: key@ira.uka.de + WWW: https://www.key-project.org/ + e-mail: support@key-project.org The KeY system is protected by the GNU General Public License. diff --git a/key.core/build.gradle b/key.core/build.gradle index f35050c9894..e0a6109475a 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -100,6 +100,7 @@ task generateSolverPropsList { list.add(file.name) } }) + list.sort() if (!file("$outputDir/$pack/solvers.txt").exists()) { String files = '' for (String propsFile : list) { 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 fd641d10982..0912e334ca8 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 @@ -237,6 +237,15 @@ private Proof(String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex } } + public Proof(String name, Term problem, String header, InitConfig initConfig, File proofFile) { + this(name, + Sequent.createSuccSequent( + Semisequent.EMPTY_SEMISEQUENT.insert(0, new SequentFormula(problem)).semisequent()), + initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig); + problemHeader = header; + this.proofFile = proofFile; + } + public Proof(String name, Term problem, String header, InitConfig initConfig) { this(name, Sequent.createSuccSequent( diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 24f41d5ac50..3b6e1192616 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -162,7 +162,8 @@ public ProofAggregate getPO() throws ProofInputException { ProofSettings settings = getPreferences(); initConfig.setSettings(settings); return ProofAggregate.createProofAggregate( - new Proof(name, problemTerm, getParseContext().getProblemHeader() + "\n", initConfig), + new Proof(name, problemTerm, getParseContext().getProblemHeader() + "\n", initConfig, + file.file()), name); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index 4d3da4e3b43..3d43b1354dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.CloseAfterMerge; /** @@ -39,12 +40,35 @@ public static ClosedBy findPreviousProof(DefaultListModel previousProofs, if (!suitableForCloseByReference(newNode)) { return null; } - DefaultListModel proofs = previousProofs; - for (int i = 0; i < proofs.size(); i++) { - Proof p = proofs.get(i); + for (int i = 0; i < previousProofs.size(); i++) { + Proof p = previousProofs.get(i); if (p == newNode.proof()) { continue; // doesn't make sense } + // conservative check: all user-defined rules in a previous proof + // have to also be available in the new proof + var proofFile = p.getProofFile() != null ? p.getProofFile().toString() : "////"; + var tacletIndex = p.allGoals().head().ruleAppIndex().tacletIndex(); + var newTacletIndex = newNode.proof().allGoals().head().ruleAppIndex().tacletIndex(); + Set newTaclets = null; + var tacletsOk = true; + for (var taclet : tacletIndex.allNoPosTacletApps().stream() + .filter(x -> x.taclet().getOrigin() != null + && x.taclet().getOrigin().contains(proofFile)) + .collect(Collectors.toList())) { + if (newTaclets == null) { + newTaclets = newTacletIndex.allNoPosTacletApps(); + } + if (newTaclets.stream().noneMatch(newTaclet -> Objects + .equals(taclet.taclet().toString(), newTaclet.taclet().toString()))) { + tacletsOk = false; + break; + } + } + if (!tacletsOk) { + continue; + } + // only search in compatible proofs if (!p.getSettings().getChoiceSettings() .equals(newNode.proof().getSettings().getChoiceSettings())) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java index babe9065a31..974cb0f1fb8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java @@ -70,6 +70,9 @@ public Proof getProof() { // display message for the status bar @Override public String toString() { + if (proof.isDisposed()) { + return "Proof disposed"; + } if (appliedRules != 0) { StringBuilder message = new StringBuilder(); String timeString = (timeInMillis / 1000) + "." + ((timeInMillis % 1000) / 100); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index 4d366d44873..c3d2634defc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -1003,9 +1003,13 @@ public TacletExecutor getExecutor() { @Override @Nullable - public String getOrigin() { return origin; } + public String getOrigin() { + return origin; + } - public void setOrigin(@Nullable String origin) { this.origin = origin; } + public void setOrigin(@Nullable String origin) { + this.origin = origin; + } public void setAddedBy(Node addedBy) { this.addedBy = addedBy; diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 091c2e56f9e..c1e7bae7889 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java @@ -2,6 +2,7 @@ import java.util.List; import java.util.Set; +import javax.swing.*; /** * This class encapsulates information about: 1) relative font size in the prover view 2) the @@ -141,6 +142,9 @@ public class ViewSettings extends AbstractPropertiesSettings { */ private static final String USER_FOLDER_BOOKMARKS = "[View]folderBookmarks"; + private static final String LOOK_AND_FEEL_DEFAULT = + UIManager.getCrossPlatformLookAndFeelClassName(); + /** * Show Taclet uninstantiated in tooltip -- for learning */ @@ -182,7 +186,8 @@ public class ViewSettings extends AbstractPropertiesSettings { private final PropertyEntry showWholeTaclet = createBooleanProperty(SHOW_WHOLE_TACLET, false); private final PropertyEntry sizeIndex = createIntegerProperty(FONT_INDEX, 2); - private final PropertyEntry lookAndFeel = createStringProperty(LOOK_AND_FEEL, null); + private final PropertyEntry lookAndFeel = + createStringProperty(LOOK_AND_FEEL, LOOK_AND_FEEL_DEFAULT); private final PropertyEntry showSequentViewTooltips = createBooleanProperty(SEQUENT_VIEW_TOOLTIP, true); private final PropertyEntry showSourceViewTooltips = diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java b/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java index 14b4989a7cb..65d4eea0cd3 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java @@ -79,4 +79,50 @@ void testFindsReferenceInSameProof() throws Exception { p.dispose(); p2.dispose(); } + + @Test + void checksUserLemmas() throws Exception { + GeneralSettings.noPruningClosed = false; + // Test scenario: + // Proof 1 uses a user-defined lemma. + // Proof 2 does not. + // Reference searcher should not find proof 1 when considering proof 2. + + KeYEnvironment env = + KeYEnvironment.load(new File(testCaseDirectory, + "proofCaching/proofWithRule.proof")); + Proof p = env.getLoadedProof(); + KeYEnvironment env2 = + KeYEnvironment.load(new File(testCaseDirectory, + "proofCaching/proofWithoutRule.proof")); + Proof p2 = env2.getLoadedProof(); + KeYEnvironment env3 = + KeYEnvironment.load(new File(testCaseDirectory, + "proofCaching/proofWithRule.proof")); + Proof p3 = env3.getLoadedProof(); + + DefaultListModel previousProofs = new DefaultListModel<>(); + previousProofs.addElement(p); + DefaultListModel newProof = new DefaultListModel<>(); + newProof.addElement(p2); + + p2.pruneProof(p2.root()); + + assertTrue(ReferenceSearcher.suitableForCloseByReference(p2.root())); + ClosedBy c = ReferenceSearcher.findPreviousProof(previousProofs, p2.root()); + assertNull(c); + + // check that result is found if the user taclet is available + p3.pruneProof(p3.root()); + assertTrue(ReferenceSearcher.suitableForCloseByReference(p3.root())); + c = ReferenceSearcher.findPreviousProof(previousProofs, p3.root()); + assertNotNull(c); + assertEquals(0, c.getNode().serialNr()); + assertEquals(p, c.getProof()); + + GeneralSettings.noPruningClosed = true; + p.dispose(); + p2.dispose(); + p3.dispose(); + } } diff --git a/key.core/src/test/resources/logback.xml b/key.core/src/test/resources/logback.xml index c96e3c9f3f3..1a1b90c6f79 100644 --- a/key.core/src/test/resources/logback.xml +++ b/key.core/src/test/resources/logback.xml @@ -6,7 +6,7 @@ key.log false - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{short}%n + %-10relative %-5level %-15thread %-25logger{5} %msg %ex%n diff --git a/key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof b/key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof new file mode 100644 index 00000000000..1c12a8e83c9 --- /dev/null +++ b/key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof @@ -0,0 +1,23 @@ +\rules { + + \lemma + two_plus_two_is_four { + \find(2 + 2 = 4) + \sameUpdateLevel + \replacewith(true) + }; + } +\problem { +add(Z(2(#)), Z(2(#))) = Z(4(#)) +} + +\proof { +(keyLog "0" (keyUser "arne" ) (keyVersion "3b3afbd3c459d500948aebed1347d8d52aa969d6")) + +(autoModeTime "0") + +(branch "dummy ID" +(rule "two_plus_two_is_four" (formula "1") (userinteraction)) +(rule "closeTrue" (formula "1") (userinteraction)) +) +} diff --git a/key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof b/key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof new file mode 100644 index 00000000000..307063856b3 --- /dev/null +++ b/key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof @@ -0,0 +1,15 @@ +\problem { +add(Z(2(#)), Z(2(#))) = Z(4(#)) +} + +\proof { +(keyLog "0" (keyUser "arne" ) (keyVersion "3b3afbd3c459d500948aebed1347d8d52aa969d6")) + +(autoModeTime "17") + +(branch "dummy ID" +(rule "add_literals" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) +(rule "closeTrue" (formula "1")) +) +} diff --git a/key.ui/examples/firstTouch/08-Java5/src/For.java b/key.ui/examples/firstTouch/08-Java5/src/For.java index f7ed037c0bb..af67d3be381 100644 --- a/key.ui/examples/firstTouch/08-Java5/src/For.java +++ b/key.ui/examples/firstTouch/08-Java5/src/For.java @@ -25,6 +25,7 @@ int sum () { void infiniteLoop() { //@ maintaining \invariant_for(f); //@ assignable \strictly_nothing; + //@ diverges true; for (Object o: f); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java index f2387302fd5..9861ae8e15c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java @@ -4,6 +4,7 @@ import java.io.IOException; import java.io.PrintStream; import java.lang.reflect.InvocationTargetException; +import java.net.URL; import java.util.ArrayList; import java.util.List; import java.util.Locale; @@ -542,9 +543,42 @@ private static AbstractMediatorUserInterfaceControl createUserInterface( public static void ensureExamplesAvailable() { File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples() : new File(getExamplesDir()); + if (!examplesDir.exists()) { + examplesDir = setupExamples(); + } setExamplesDir(examplesDir.getAbsolutePath()); } + private static File setupExamples() { + try { + URL examplesURL = Main.class.getResource("/examples.zip"); + if (examplesURL == null) { + throw new IOException("Missing examples.zip in resources"); + } + + File tempDir = createTempDirectory(); + + if (tempDir != null) { + IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath()); + } + return tempDir; + } catch (IOException e) { + LOGGER.warn("Error setting up examples", e); + return null; + } + } + + + private static File createTempDirectory() throws IOException { + final File tempDir = File.createTempFile("keyheap-examples-", null); + tempDir.delete(); + if (!tempDir.mkdir()) { + return null; + } + Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir))); + return tempDir; + } + private static void evaluateLemmataOptions(CommandLine options) { LemmataAutoModeOptions opt; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java index 5249c1752ba..b64ad30f68b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java @@ -35,7 +35,11 @@ private Watchdog() { * Start the watchdog in a background thread. */ public static void start() { - new Thread(Watchdog::run, "Watchdog").start(); + var thread = new Thread(Watchdog::run, "Watchdog"); + // mark as daemon + // (only relevant for startup exception, where this thread would prevent the JVM exiting) + thread.setDaemon(true); + thread.start(); } private static void run() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java index dbeea424c25..17d90432e74 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java @@ -163,6 +163,7 @@ public HeatmapOptionsDialog() { pack(); setAlwaysOnTop(true); setResizable(false); + setLocationRelativeTo(MainWindow.getInstance()); } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 2a9afc727af..94a2898b027 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -546,11 +546,15 @@ private JPanel createSourcePanel(Font font) { /** * Shows the dialog with a single exception. The stacktrace is extracted and can optionally be * shown in the dialog. + * Important: make sure to also log the exception before showing the dialog! * * @param parent the parent of the dialog (will be blocked) * @param exception the exception to display */ public static void showExceptionDialog(Window parent, Throwable exception) { + // make sure UI is usable after any exception + MainWindow.getInstance().getMediator().startInterface(true); + Set msg = Collections.singleton(extractMessage(exception)); IssueDialog dlg = new IssueDialog(parent, "Parser Error", msg, true, exception); dlg.setVisible(true); 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 62915893971..019181df058 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 @@ -45,6 +45,7 @@ import de.uka.ilkd.key.gui.plugins.action_history.ActionHistoryExtension; import de.uka.ilkd.key.gui.proofdiff.ProofDiffFrame; import de.uka.ilkd.key.gui.prooftree.ProofTreeView; +import de.uka.ilkd.key.gui.settings.FontSizeFacade; import de.uka.ilkd.key.gui.settings.SettingsManager; import de.uka.ilkd.key.gui.smt.DropdownSelectionButton; import de.uka.ilkd.key.gui.sourceview.SourceViewFrame; @@ -58,6 +59,7 @@ import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.ViewSettings; import de.uka.ilkd.key.smt.SolverTypeCollection; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; @@ -287,6 +289,9 @@ private MainWindow() { mediator = getMainWindowMediator(userInterface); KeYGuiExtensionFacade.getStartupExtensions().forEach(it -> it.preInit(this, mediator)); + ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); + FontSizeFacade.resizeFonts(vs.getUIFontSizeFactor()); + termLabelMenu = new TermLabelMenu(this); currentGoalView = new CurrentGoalView(this); emptySequent = new EmptySequent(this); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java index daaf1a32c91..8f7f413a826 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java @@ -118,6 +118,7 @@ protected void done() { if (!isCancelled() && exception != null) { // user cancelled task is fine, we do not // report this // This should actually never happen. + LOGGER.error("", exception); IssueDialog.showExceptionDialog(MainWindow.getInstance(), exception); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java index cf653b9255a..9effcd984c2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java @@ -44,9 +44,13 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + public final class ProofManagementDialog extends JDialog { private static final long serialVersionUID = 3543411893273433386L; + private static final Logger LOGGER = LoggerFactory.getLogger(ProofManagementDialog.class); /** * The contracts are stored by name of the {@link KeYJavaType}, method name, and contract name @@ -476,15 +480,20 @@ private void findOrStartProof(@Nonnull Contract contract) { env = ui.createProofEnvironmentAndRegisterProof(po, pl, initConfig); } else { env.registerProof(po, pl); - } } catch (ProofInputException exc) { + LOGGER.error("", exc); IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); } } else { mediator.setProof(proof); } startedProof = true; + // starting another proof will not execute the ProblemLoader again, + // so we have to activate the UI here + if (initConfig.getServices().getSpecificationRepository().getAllProofs().size() > 1) { + mediator.startInterface(true); + } } private void updateStartButton() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java index ef71a3230c6..eaed97d7a42 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java @@ -170,6 +170,7 @@ public void done() { } catch (CancellationException ex) { LOGGER.info("Scripting was cancelled."); } catch (Throwable ex) { + LOGGER.error("", ex); IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java index bc732d4521d..0a427a7eb0e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java @@ -14,6 +14,9 @@ import javax.swing.*; import javax.swing.border.TitledBorder; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * This dialog allows the user to select the proof to load from a proof bundle. * @@ -22,6 +25,7 @@ public final class ProofSelectionDialog extends JDialog { private static final long serialVersionUID = -586107341789859969L; + private static final Logger LOGGER = LoggerFactory.getLogger(ProofSelectionDialog.class); /** * Regex for identifiers (class, method), which catches for example "java.lang.Object", @@ -203,6 +207,7 @@ private static Path showDialog(Path bundlePath) { dialog.setVisible(true); proofPath = dialog.proofToLoad; } catch (IOException exc) { + LOGGER.error("", exc); IssueDialog.showExceptionDialog(MainWindow.getInstance(), exc); } return proofPath; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 538bf4f2e03..05eeef2941f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -242,6 +242,8 @@ public String getMostRecent() { */ public void store(String filename) { File localRecentFiles = new File(filename); + localRecentFiles.getParentFile().mkdirs(); + // creates a new file if it does not exist yet try { localRecentFiles.createNewFile(); @@ -257,7 +259,7 @@ public void store(String filename) { store(p); p.store(fout, "recent files"); } catch (IOException ex) { - LOGGER.info("Could not write recent files list", ex); + LOGGER.info("Could not write recent files list ", ex); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java index 6eaf41deeb7..f5b944d0249 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java @@ -118,9 +118,10 @@ public Node nextNode() { while (previous != null && (previous.proof().isDisposed() || !previous.proof().find(previous) || previous == currentSelection)) { - previous = selectionHistoryForward.removeLast(); + previous = !selectionHistoryForward.isEmpty() ? selectionHistoryForward.removeLast() + : null; } - // this is a query method, re-instantiate previous state + // this is a query method (modulo fixing up the history), re-instantiate previous state if (previous != null) { selectionHistoryForward.addLast(previous); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java index 4de95d9f3a4..2eee26ddf36 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java @@ -321,6 +321,7 @@ public void actionPerformed(ActionEvent e) { errorPositionKnown(exc.getMessage(), ex.getPosition().line(), ex.getPosition().column(), ex.inIfSequent()); } + LOGGER.error("", exc); IssueDialog.showExceptionDialog(TacletMatchCompletionDialog.this, exc); return; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index dd5e384ab8f..c01a0431999 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -149,6 +149,11 @@ public void resetStatus(Object sender) { @Override public void taskFinished(TaskFinishedInfo info) { super.taskFinished(info); + // ensure all UI modifying operations are done on the UI thread + SwingUtilities.invokeLater(() -> taskFinishedInternal(info)); + } + + private void taskFinishedInternal(TaskFinishedInfo info) { if (info != null && info.getSource() instanceof ProverCore) { if (!isAtLeastOneMacroRunning()) { resetStatus(this); @@ -156,7 +161,7 @@ public void taskFinished(TaskFinishedInfo info) { ApplyStrategyInfo result = (ApplyStrategyInfo) info.getResult(); Proof proof = info.getProof(); - if (proof != null && !proof.closed() + if (proof != null && !proof.isDisposed() && !proof.closed() && mainWindow.getMediator().getSelectedProof() == proof) { Goal g = result.nonCloseableGoal(); if (g == null) { @@ -194,6 +199,7 @@ public void taskFinished(TaskFinishedInfo info) { resetStatus(this); Throwable result = (Throwable) info.getResult(); if (info.getResult() != null) { + LOGGER.error("", result); IssueDialog.showExceptionDialog(mainWindow, result); } else if (getMediator().getUI().isSaveOnly()) { mainWindow.displayResults("Finished Saving!"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AbandonTaskAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AbandonTaskAction.java index 5c2c6dee159..d2ff95a41b7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AbandonTaskAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AbandonTaskAction.java @@ -32,6 +32,10 @@ public AbandonTaskAction(MainWindow mainWindow, Proof proof) { public synchronized void actionPerformed(ActionEvent e) { boolean removalConfirmed = getMediator().getUI().confirmTaskRemoval("Are you sure?"); if (removalConfirmed) { + // abandon proof that is currently in auto mode: first stop auto mode + if (getMediator().isInAutoMode()) { + getMediator().getUI().getProofControl().stopAutoMode(); + } if (proof == null) { getMediator().getSelectedProof().dispose(); } else { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java index f1c737a110c..2ffe2b3578c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java @@ -7,23 +7,19 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; /** + * Action to select the next goal above in the proof tree. */ public final class GoalSelectAboveAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = 4574670781882014092L; /** - * Creates a new GoalBackAction. + * Creates the new action. * * @param mainWindow the main window this action belongs to - * @param longName true iff long names (including the name of the rule to undo) shall be - * displayed (e.g. in menu items) */ public GoalSelectAboveAction(MainWindow mainWindow) { - super(mainWindow); + super(mainWindow, true); setAcceleratorLetter(KeyEvent.VK_K); setName("Select Goal Above"); setIcon(IconFactory.selectGoalAbove(MainWindow.TOOLBAR_ICON_SIZE)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java index aba46f051dc..e655ae4708b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java @@ -7,23 +7,19 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; /** + * Action to select the next goal below in the proof tree. */ public final class GoalSelectBelowAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = 4574670781882014092L; /** - * Creates a new GoalBackAction. + * Creates the new action. * * @param mainWindow the main window this action belongs to - * @param longName true iff long names (including the name of the rule to undo) shall be - * displayed (e.g. in menu items) */ public GoalSelectBelowAction(MainWindow mainWindow) { - super(mainWindow); + super(mainWindow, true); setAcceleratorLetter(KeyEvent.VK_J); setName("Select Goal Below"); setIcon(IconFactory.selectGoalBelow(MainWindow.TOOLBAR_ICON_SIZE)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java index 42ee7069843..a0fc83ef3ff 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java @@ -25,7 +25,12 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + public abstract class LemmaGenerationAction extends MainWindowAction { + private static final Logger LOGGER = LoggerFactory.getLogger(LemmaGenerationAction.class); + public enum Mode { ProveUserDefinedTaclets, ProveKeYTaclets, ProveAndAddUserDefinedTaclets } @@ -53,6 +58,7 @@ public LemmaGenerationAction(MainWindow mainWindow) { abstract protected boolean proofIsRequired(); protected final void handleException(Throwable exception) { + LOGGER.error("", exception); IssueDialog.showExceptionDialog(mainWindow, exception); } @@ -134,6 +140,7 @@ protected void loadTaclets() { LoaderListener listener = new AbstractLoaderListener(mainWindow) { @Override public void doStopped(Throwable exception) { + LOGGER.error("", exception); IssueDialog.showExceptionDialog(ProveKeYTaclets.this.mainWindow, exception); } @@ -213,6 +220,7 @@ protected void loadTaclets() { LoaderListener listener = new AbstractLoaderListener(mainWindow) { @Override public void doStopped(Throwable exception) { + LOGGER.error("", exception); IssueDialog.showExceptionDialog(ProveUserDefinedTaclets.this.mainWindow, exception); } @@ -287,6 +295,7 @@ protected void loadTaclets() { LoaderListener listener = new AbstractLoaderListener(mainWindow) { @Override public void doStopped(Throwable exception) { + LOGGER.error("", exception); IssueDialog.showExceptionDialog(ProveAndAddTaclets.this.mainWindow, exception); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java index 81c6b38525c..40206950333 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java @@ -1,8 +1,12 @@ package de.uka.ilkd.key.gui.actions; +import java.util.ArrayList; +import java.util.Collection; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.core.KeYSelectionEvent; +import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; @@ -12,11 +16,11 @@ * {@link KeyStrokeManager}. */ public abstract class MainWindowAction extends KeyAction { - /** - * - */ private static final long serialVersionUID = -6611537258325987383L; + private static final MainWindowActionSelectionListener LISTENER = + new MainWindowActionSelectionListener(); + protected final MainWindow mainWindow; protected MainWindowAction(MainWindow mainWindow) { @@ -26,6 +30,14 @@ protected MainWindowAction(MainWindow mainWindow) { KeyStrokeManager.registerAction(this); } + protected MainWindowAction(MainWindow mainWindow, boolean onlyActiveWhenProofAvailable) { + this(mainWindow); + if (onlyActiveWhenProofAvailable) { + LISTENER.addAction(this); + this.setEnabled(getMediator().getSelectionModel().getSelectedProof() != null); + } + } + protected void setAcceleratorLetter(int letter) { setAcceleratorKey(KeyStroke.getKeyStroke(letter, SHORTCUT_KEY_MASK)); } @@ -41,4 +53,26 @@ protected void setAcceleratorKey(KeyStroke keyStroke) { protected KeYMediator getMediator() { return mainWindow.getMediator(); } + + private static final class MainWindowActionSelectionListener implements KeYSelectionListener { + private final Collection actions = new ArrayList<>(); + + private void addAction(MainWindowAction action) { + if (actions.isEmpty()) { + action.getMediator().addKeYSelectionListener(this); + } + actions.add(action); + } + + @Override + public void selectedNodeChanged(KeYSelectionEvent e) { + var enable = e.getSource().getSelectedProof() != null; + actions.forEach(a -> a.setEnabled(enable)); + } + + @Override + public void selectedProofChanged(KeYSelectionEvent e) { + selectedNodeChanged(e); + } + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java index 7c85129edd1..e2aede274fb 100755 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java @@ -11,6 +11,9 @@ import de.uka.ilkd.key.gui.ProofScriptWorker; import de.uka.ilkd.key.proof.Proof; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * The Class ProofScriptFromFileAction. * @@ -18,6 +21,7 @@ */ public class ProofScriptFromFileAction extends AbstractAction { private static final long serialVersionUID = -3181592516055470032L; + private static final Logger LOGGER = LoggerFactory.getLogger(ProofScriptFromFileAction.class); private final KeYMediator mediator; @@ -66,6 +70,7 @@ public void actionPerformed(ActionEvent e) { psw.execute(); } } catch (Exception ex) { + LOGGER.error("", ex); IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 72116827dca..7290c18d0dd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -356,6 +356,7 @@ public String getDescription() { + "e-mail to " + FEEDBACK_RECIPIENT + ".", jfc.getSelectedFile())); } } catch (Exception e) { + LOGGER.error("", e); IssueDialog.showExceptionDialog(parent, e); } } @@ -399,6 +400,7 @@ private void sendReport(String message) { } } catch (Exception e) { + LOGGER.error("", e); IssueDialog.showExceptionDialog(parent, e); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeManager.java index b7fedd992a1..94dc623fcaa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeManager.java @@ -3,6 +3,7 @@ import java.awt.*; import java.awt.event.KeyEvent; import java.lang.ref.WeakReference; +import java.util.Collection; import java.util.HashMap; import java.util.Map; import javax.swing.*; @@ -160,4 +161,13 @@ private static int getShortcutMask() { return 0; } } + + /** + * Get all the managed actions. + * + * @return all actions + */ + public static Collection> getAllActions() { + return actions.values(); + } } 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 49fdaf6d911..834679e6d5f 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 @@ -263,9 +263,9 @@ private JDialog getHelpWindow() { textArea.setEditable(false); helpWindow.getContentPane().add(new JScrollPane(textArea)); helpWindow.setMinimumSize(new Dimension(400, 200)); - helpWindow.setLocationRelativeTo(MainWindow.getInstance()); helpWindow.setTitle("Help"); helpWindow.pack(); + helpWindow.setLocationRelativeTo(MainWindow.getInstance()); } return helpWindow; @@ -448,8 +448,8 @@ private JDialog getDialog() { buttonPane.add(Box.createHorizontalStrut(5)); buttonPane.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); pane.add(buttonPane); - dialog.setLocationRelativeTo(MainWindow.getInstance()); dialog.pack(); + dialog.setLocationRelativeTo(MainWindow.getInstance()); } return dialog; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java index e285be36bbb..662363ceb43 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java @@ -7,7 +7,12 @@ import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + public class ExceptionFailureNotificationDialog extends ShowDisplayPane { + private static final Logger LOGGER = + LoggerFactory.getLogger(ExceptionFailureNotificationDialog.class); public ExceptionFailureNotificationDialog(Frame parentComponent) { super(parentComponent); @@ -18,6 +23,7 @@ public boolean execute(NotificationEvent event) { if (event instanceof ExceptionFailureEvent) { ExceptionFailureEvent ev = (ExceptionFailureEvent) event; setMessage(ev.getErrorMessage()); + LOGGER.error(ev.getErrorMessage(), ev.getException()); IssueDialog.showExceptionDialog(parentComponent, ev.getException()); } else { setMessage("An unknown error has occured." + event); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/events/GeneralFailureEvent.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/events/GeneralFailureEvent.java index 584f5852bc5..1595ad968b4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/events/GeneralFailureEvent.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/events/GeneralFailureEvent.java @@ -9,8 +9,10 @@ * A notification event caused by a general unexpected failure (usually caused by a bug of the * system) * + * @deprecated use {@link de.uka.ilkd.key.gui.IssueDialog} * @author bubel */ +@Deprecated public class GeneralFailureEvent extends NotificationEvent { private String errorMessage = "Unknown Error."; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java index 6ce2a336f10..3077e23a9c8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java @@ -69,6 +69,7 @@ public class CachingExtension * Proofs tracked for automatic reference search. */ private final Set trackedProofs = new HashSet<>(); + private ReferenceSearchButton referenceSearchButton; @Override public void selectedProofChanged(KeYSelectionEvent e) { @@ -156,7 +157,8 @@ public List getContextActions(@Nonnull KeYMediator mediator, @Override public List getStatusLineComponents() { - return List.of(new ReferenceSearchButton(mediator)); + referenceSearchButton = new ReferenceSearchButton(mediator); + return List.of(referenceSearchButton); } @Override @@ -181,7 +183,7 @@ public void taskFinished(TaskFinishedInfo info) { return; // try close macro was running, no need to do anything here } Proof p = info.getProof(); - if (p == null || p.closed() || !(info.getSource() instanceof ApplyStrategy + if (p == null || p.isDisposed() || p.closed() || !(info.getSource() instanceof ApplyStrategy || info.getSource() instanceof ProofMacro)) { return; } @@ -263,7 +265,7 @@ public void proofDisposed(ProofDisposedEvent e) { * * @author Arne Keller */ - static class CloseByReference extends KeyAction { + private final class CloseByReference extends KeyAction { /** * The mediator. */ @@ -311,6 +313,9 @@ public void actionPerformed(ActionEvent e) { mismatches.add(n.serialNr()); } } + if (!nodes.isEmpty()) { + referenceSearchButton.updateState(nodes.get(0).proof()); + } if (!mismatches.isEmpty()) { JOptionPane.showMessageDialog((JComponent) e.getSource(), "No matching branch found for node(s) " + Arrays.toString(mismatches.toArray()), diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index ecd65c5cce1..3e2ff836483 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -69,6 +69,15 @@ public void actionPerformed(ActionEvent e) { @Override public void selectedNodeChanged(KeYSelectionEvent e) { Proof p = e.getSource().getSelectedProof(); + updateState(p); + } + + /** + * Update the UI state of this button. + * + * @param p the currently selected proof + */ + public void updateState(Proof p) { if (p == null) { setText("Proof Caching"); setForeground(null); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java index d37782cb47e..fdaca1743cb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java @@ -10,6 +10,9 @@ import org.key_project.util.java.SwingUtil; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Dialog showing reference search information. * @@ -18,6 +21,8 @@ public class ReferenceSearchDialog extends JDialog { private static final long serialVersionUID = 1L; + private static final Logger LOGGER = LoggerFactory.getLogger(ReferenceSearchDialog.class); + /** * The table of reference search results. */ @@ -107,6 +112,7 @@ private JButton getApplyButton() { listener.copyButtonClicked(this); } catch (Exception exception) { // There may be exceptions during rule application that should not be lost. + LOGGER.error("", exception); IssueDialog.showExceptionDialog(ReferenceSearchDialog.this, exception); } }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java index 17eb2b81aa9..b0781ff1f4f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java @@ -3,6 +3,7 @@ import java.awt.*; import java.util.Collections; import java.util.List; +import java.util.stream.Collectors; import javax.swing.*; import javax.swing.event.TableModelEvent; import javax.swing.event.TableModelListener; @@ -24,9 +25,9 @@ class ReferenceSearchTable extends JTable implements TableModel { */ private final KeYMediator mediator; /** - * List of open goals in the selected proof. + * List of open and closed goals in the selected proof. */ - private final List openGoals; + private final List goals; /** * Construct a new table. @@ -36,8 +37,10 @@ class ReferenceSearchTable extends JTable implements TableModel { */ public ReferenceSearchTable(Proof proof, KeYMediator mediator) { this.setModel(this); - this.openGoals = proof.openGoals().toList(); - Collections.reverse(this.openGoals); + this.goals = proof.allGoals().stream() + .filter(g -> !g.node().isClosed() || g.node().lookup(ClosedBy.class) != null) + .collect(Collectors.toList()); + Collections.reverse(this.goals); this.mediator = mediator; getColumnModel().getColumn(1).setMinWidth(200); } @@ -60,7 +63,7 @@ public void removeTableModelListener(TableModelListener l) { @Override public int getRowCount() { - return openGoals.size(); + return goals.size(); } @Override @@ -88,9 +91,9 @@ public Class getColumnClass(int column) { @Override public Object getValueAt(int row, int column) { if (column == 0) { - return String.valueOf(openGoals.get(row).node().serialNr()); + return String.valueOf(goals.get(row).node().serialNr()); } else { - Goal g = openGoals.get(row); + Goal g = goals.get(row); ClosedBy c = g.node().lookup(ClosedBy.class); if (c == null) { return "no reference found"; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java index de63ce022ca..f167a1f7535 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java @@ -32,6 +32,9 @@ public void setVisible(boolean vis) { public void searchNext() { fillCache(); + if (cache.isEmpty()) { + return; // no results to switch to + } startRow = currentRow + 1; startRow %= cache.size(); search(searchField.getText(), Position.Bias.Forward); @@ -39,6 +42,9 @@ public void searchNext() { public void searchPrevious() { fillCache(); + if (cache.isEmpty()) { + return; // no results to switch to + } startRow = currentRow - 1; startRow %= cache.size(); search(searchField.getText(), Position.Bias.Backward); @@ -98,7 +104,8 @@ private void addNodeToCache(GUIAbstractTreeNode node) { private void fillCache() { if (cache == null) { cache = new ArrayList<>(); - if (this.proofTreeView.delegateModel.getRoot() != null) { + if (this.proofTreeView.delegateModel != null + && this.proofTreeView.delegateModel.getRoot() != null) { addNodeToCache((GUIAbstractTreeNode) this.proofTreeView.delegateModel.getRoot()); fillCacheHelp((GUIBranchNode) this.proofTreeView.delegateModel.getRoot()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java index 81784e6e0d5..a04baa361a1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java @@ -54,16 +54,14 @@ private static CButton createExpandAll(ProofTreeView view) { } private static CCheckBox createFilter(ProofTreeView view, ProofTreeViewFilter filter) { - CCheckBox check = new CCheckBox() { - @Override - protected void changed() { - final boolean selected = isSelected(); - setEnabled(view.setFilter(filter, selected)); - } - }; + CCheckBox check = new ProofTreeSettingsCheckBox(); check.setText(filter.name()); check.setEnabled(view.delegateModel != null); check.setSelected(filter.isActive()); + // add the selection listener *after* setting the initial value + // (to avoid re-applying the filter) + check.intern().addSelectableListener( + (component, selected) -> check.setEnabled(view.setFilter(filter, check.isSelected()))); return check; } @@ -132,4 +130,17 @@ protected void changed() { check.setSelected(MainWindow.getInstance().isShowTacletInfo()); return check; } + + /** + * The checkbox used in the proof tree settings. + * + * @author Arne Keller + */ + private static class ProofTreeSettingsCheckBox extends CCheckBox { + @Override + protected void changed() { + // intentionally empty, a listener is added in the menu factory + } + } + } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index e09f8339590..f2157f220bc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -325,6 +325,7 @@ private void setProofTreeFont() { // set row height before changing the font (since the latter repaints the component) delegateView.setRowHeight(rowHeight); + renderer.setFont(myFont); delegateView.setFont(myFont); } else { LOGGER.debug("KEY-PROOF_TREE_FONT not available, use standard font."); @@ -392,21 +393,65 @@ private void unregister() { mediator.removeGUIListener(guiListener); } + /** + * Select the next goal above the currently selected node. + * + * @return whether such a goal was found + */ public boolean selectAbove() { - return selectRelative(+1); + TreePath path = delegateView.getSelectionPath(); + if (path == null) { + return false; + } + int row = delegateView.getRowForPath(path); + row--; + while (delegateView.getPathForRow(row) != null) { + TreePath tp = delegateView.getPathForRow(row); + var treeNode = (GUIAbstractTreeNode) tp.getLastPathComponent(); + if (treeNode instanceof GUIBranchNode && treeNode.getNode().parent() != null + && treeNode.getNode().parent().childrenCount() > 1 + && !delegateView.isExpanded(tp)) { + int prevRows = delegateView.getRowCount(); + delegateView.expandPath(tp); + int newRows = delegateView.getRowCount(); + // search must continue at the end of the just expanded branch! + row += (newRows - prevRows); + continue; + } + if (treeNode.getNode().leaf()) { + mediator.getSelectionModel().setSelectedNode(treeNode.getNode()); + return true; + } + row--; + } + return false; } + /** + * Select the next goal below the currently selected node. + * + * @return whether such a goal was found + */ public boolean selectBelow() { - return selectRelative(-1); - } - - private boolean selectRelative(int i) { TreePath path = delegateView.getSelectionPath(); + if (path == null) { + return false; + } int row = delegateView.getRowForPath(path); - TreePath newPath = delegateView.getPathForRow(row - i); - if (newPath != null) { - delegateView.setSelectionPath(newPath); - return true; + row++; + while (delegateView.getPathForRow(row) != null) { + TreePath tp = delegateView.getPathForRow(row); + var treeNode = (GUIAbstractTreeNode) tp.getLastPathComponent(); + if (treeNode instanceof GUIBranchNode && treeNode.getNode().parent() != null + && treeNode.getNode().parent().childrenCount() > 1 + && !delegateView.isExpanded(tp)) { + delegateView.expandPath(tp); + } + if (treeNode.getNode().leaf()) { + mediator.getSelectionModel().setSelectedNode(treeNode.getNode()); + return true; + } + row++; } return false; } @@ -678,6 +723,10 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) { return false; } + // Save expansion state to restore. + List rowsToExpand = new ArrayList<>(expansionState); + + final TreePath branch; final Node invokedNode; if (selectedPath.getLastPathComponent() instanceof GUIProofTreeNode) { @@ -741,6 +790,17 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) { delegateView.setSelectionPath(tp); } } + + // Expand previously visible rows. + for (TreePath tp : rowsToExpand) { + TreePath newTp = delegateView.getPathForRow(0); + for (int i = 1; i < tp.getPathCount(); i++) { + Node n = ((GUIBranchNode) tp.getPathComponent(i)).getNode(); + newTp = newTp.pathByAddingChild( + delegateModel.getBranchNode(n, n.getNodeInfo().getBranchLabel())); + } + delegateView.expandPath(newTp); + } return true; } @@ -921,6 +981,10 @@ public void valueChanged(TreeSelectionEvent e) { GUIAbstractTreeNode treeNode = ((GUIAbstractTreeNode) e.getNewLeadSelectionPath().getLastPathComponent()); + if (treeNode.getNode().proof().isDisposed()) { + setProof(null); + return; + } if (treeNode instanceof GUIBranchNode) { selectBranchNode((GUIBranchNode) treeNode); } else { @@ -1210,7 +1274,7 @@ private void renderOneStepSimplification(Style style, GUIOneStepChildTreeNode no @Override public Component getTreeCellRendererComponent(JTree tree, Object value, boolean sel, boolean expanded, boolean leaf, int row, boolean hasFocus) { - if (proof == null || !(value instanceof GUIAbstractTreeNode)) { + if (proof == null || proof.isDisposed() || !(value instanceof GUIAbstractTreeNode)) { // print dummy tree return super.getTreeCellRendererComponent(tree, value, sel, expanded, leaf, row, hasFocus); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FontSizeFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FontSizeFacade.java index 36b38be4187..a7536df4add 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FontSizeFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FontSizeFacade.java @@ -5,6 +5,10 @@ import java.util.Map; import javax.swing.*; +import de.uka.ilkd.key.gui.MainWindow; + +import org.key_project.util.java.SwingUtil; + /** * @author Alexander Weigl * @version 1 (10.05.19) @@ -22,14 +26,14 @@ public class FontSizeFacade { "Slider.font", "Spinner.font", "TabbedPane.font", "TabbedPane.smallFont", "Table.font", "TableHeader.font", "TextArea.font", "TextField.font", "TextPane.font", "TitledBorder.font", "ToggleButton.font", "ToolBar.font", "ToolTip.font", "Tree.font", "Viewport.font" }; - private static final Map originalFontSize = new HashMap<>(); + private static final Map originalFontSize = new HashMap<>(); private static double currentFactor = 1; public static void saveCurrentFontSizes() { for (String k : KEYS) { Font f = UIManager.getDefaults().getFont(k); if (f != null) { - originalFontSize.put(k, f.getSize()); + originalFontSize.put(k, (float) f.getSize()); } } } @@ -56,14 +60,13 @@ public static void resizeFonts(double factor) { } }); - // redraw all frames - for (Window w : Window.getWindows()) { - SwingUtilities.updateComponentTreeUI(w); - } + // for some reason, the menu bar does not update its font on its own + SwingUtil.setFont(MainWindow.getInstance().getJMenuBar(), + UIManager.getDefaults().getFont("Menu.font")); - for (Window w : Dialog.getWindows()) { + // redraw all frames and dialogs + for (Window w : Window.getWindows()) { SwingUtilities.updateComponentTreeUI(w); } - } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index 5cc0a631498..24ee00bef2b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java @@ -11,6 +11,9 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * The settings dialog. * @@ -20,6 +23,8 @@ */ public class SettingsDialog extends JDialog { private static final long serialVersionUID = -3204453471778351602L; + private static final Logger LOGGER = LoggerFactory.getLogger(SettingsDialog.class); + private final MainWindow mainWindow; private final SettingsUi ui; private final Action actionCancel = new CancelAction(); @@ -86,6 +91,9 @@ private void apply(List providers, List exceptions) private boolean showErrors(List apply) { if (!apply.isEmpty()) { + for (Exception e : apply) { + LOGGER.error("", e); + } String msg = apply.stream().map(Throwable::getMessage) .collect(Collectors.joining("
", "", "")); JOptionPane.showMessageDialog(this, msg, "Error in Settings", diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 45ce5e35d21..24f814c9841 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -17,12 +17,17 @@ import org.key_project.util.java.SwingUtil; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Dialog showing launched SMT processes and results. */ public class ProgressDialog extends JDialog { private static final long serialVersionUID = 1L; + private static final Logger LOGGER = LoggerFactory.getLogger(ProgressDialog.class); + private final ProgressTable table; /** * Button to apply the results of running the SMT solver. @@ -89,7 +94,6 @@ public ProgressDialog(ProgressModel model, ProgressDialogListener listener, table.getTableHeader().setReorderingAllowed(false); table.setModel(model, titles); this.listener = listener; - setLocationRelativeTo(MainWindow.getInstance()); if (counterexample) { this.setTitle("SMT Counterexample Search"); } else { @@ -126,6 +130,8 @@ public ProgressDialog(ProgressModel model, ProgressDialogListener listener, constraints.insets.bottom = 5; contentPane.add(buttonBox, constraints); this.pack(); + // always set the location last, otherwise it is not centered! + setLocationRelativeTo(MainWindow.getInstance()); } public void setProgress(int value) { @@ -151,6 +157,7 @@ private JButton getFocusButton() { try { listener.focusButtonClicked(); } catch (Exception exception) { + LOGGER.error("", exception); // There may be exceptions during rule application that should not be lost. IssueDialog.showExceptionDialog(ProgressDialog.this, exception); } @@ -170,6 +177,7 @@ private JButton getApplyButton() { listener.applyButtonClicked(); } catch (Exception exception) { // There may be exceptions during rule application that should not be lost. + LOGGER.error("", exception); IssueDialog.showExceptionDialog(ProgressDialog.this, exception); } }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java index d5975630dd8..1ca0b5be905 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java @@ -9,6 +9,8 @@ import de.uka.ilkd.key.control.AbstractProofControl; import de.uka.ilkd.key.control.ProofControl; import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.IssueDialog; +import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofMacroWorker; import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent; import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; @@ -196,6 +198,10 @@ protected void done() { ui.getMediator().startInterface(true); emitInteractiveAutoMode(initialGoals, proof, info); + + if (info.getException() != null) { + notifyException(info.getException()); + } } } @@ -204,9 +210,9 @@ protected void emitInteractiveAutoMode(List initialGoals, Proof proof, interactionListeners.forEach((l) -> l.runAutoMode(initialGoals, proof, info)); } - private void notifyException(final Exception exception) { - ui.notify(new GeneralFailureEvent( - "An exception occurred during" + " strategy execution.\n Exception:" + exception)); + private void notifyException(final Throwable exception) { + LOGGER.error("exception during strategy ", exception); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), exception); } @Override diff --git a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java new file mode 100644 index 00000000000..c6c51f86734 --- /dev/null +++ b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java @@ -0,0 +1,176 @@ +package org.key_project.util.java; + + +import java.awt.*; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import javax.swing.*; + +import bibliothek.gui.dock.themes.basic.BasicDockableDisplayer; + +/** + * Utilities for working with Swing. + * + * @author Arne Keller + */ +public final class SwingUtil { + private SwingUtil() { + } + + /** + * Find a component of the specified class in the container. + * This will search the view hierarchy recursively. + * + * @param container container to search in + * @param classToFind class to look for + * @return the object if found, otherwise null + * @param class of the component + */ + public static T findComponent(Container container, Class classToFind) { + for (int i = 0; i < container.getComponentCount(); i++) { + var c = container.getComponent(i); + if (c.getClass().equals(classToFind)) { + return (T) c; + } else if (c instanceof Container) { + var f = findComponent((Container) c, classToFind); + if (f != null) { + return f; + } + } + } + return null; + } + + /** + * Find all components of the specified class in the container. + * This will search the view hierarchy recursively and is limited + * to "visible" elements (on screen or on visible tab). + * + * @param container container to search in + * @param classToFind class to look for + * @return the object(s) if found (may be empty) + * @param class of the component + */ + public static List findAllComponents(Container container, Class classToFind) { + List l = new ArrayList<>(); + for (int i = 0; i < container.getComponentCount(); i++) { + var c = container.getComponent(i); + // if the docking container is visible, we consider all tabs in the search + if (!c.isVisible() && !(c instanceof BasicDockableDisplayer)) { + continue; + } + + if (classToFind.isAssignableFrom(c.getClass())) { + l.add((T) c); + } else if (c instanceof Container) { + var f = findAllComponents((Container) c, classToFind); + l.addAll(f); + } + if (c instanceof JMenu) { + var queue = new HashSet(); + queue.add((JMenu) c); + while (!queue.isEmpty()) { + var newQ = new HashSet(); + for (var menu : queue) { + for (int j = 0; j < menu.getItemCount(); j++) { + var item = menu.getItem(j); + if (item == null) { + continue; + } + if (item instanceof JMenu) { + newQ.add((JMenu) item); + } + if (classToFind.isAssignableFrom(item.getClass())) { + l.add((T) item); + } + } + } + queue = newQ; + } + } + } + return l; + } + + public static Collection getAllOpenWindows() { + var l = new HashSet(); + + Set q = new HashSet<>(); + q.addAll(Arrays.asList(Window.getWindows())); + q.addAll(Arrays.asList(Window.getOwnerlessWindows())); + while (!q.isEmpty()) { + var newQ = new HashSet(); + + for (var window : q) { + if (l.contains(window)) { + continue; + } + l.add(window); + newQ.addAll(Arrays.asList(window.getOwnedWindows())); + } + q = newQ; + } + + return l; + } + + public static List getPopups() { + MenuSelectionManager msm = MenuSelectionManager.defaultManager(); + MenuElement[] p = msm.getSelectedPath(); + + List list = new ArrayList<>(); + for (MenuElement element : p) { + if (element instanceof JPopupMenu) { + list.add((JPopupMenu) element); + } + } + return list; + } + + /** + * Create a scroll pane around the given table. + * It will always have vertical and horizontal scroll bars. + * + * @param table the table + * @return the scroll pane + */ + public static JScrollPane createScrollPane(JTable table) { + var scrollPane = new JScrollPane(table, ScrollPaneConstants.VERTICAL_SCROLLBAR_ALWAYS, + ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS); + + Dimension dim = new Dimension(table.getPreferredSize()); + dim.width += (Integer) UIManager.get("ScrollBar.width") + 2; + dim.height = scrollPane.getPreferredSize().height; + scrollPane.setPreferredSize(dim); + + return scrollPane; + } + + /** + * Set the provided font on the component and recursively on all children components. + * + * @param component the component + * @param font the font + */ + public static void setFont(JComponent component, Font font) { + component.setFont(font); + for (int i = 0; i < component.getComponentCount(); i++) { + Component c = component.getComponent(i); + if (c == null) { + continue; + } + c.setFont(font); + if (c instanceof JComponent) { + setFont((JComponent) c, font); + } + } + // JMenu hides its entries in the popup menu + if (component instanceof JMenu && ((JMenu) component).getPopupMenu() != null) { + setFont(((JMenu) component).getPopupMenu(), font); + } + } +} diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java new file mode 100644 index 00000000000..67b9dea1057 --- /dev/null +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java @@ -0,0 +1,224 @@ +package de.uka.ilkd.key.gui; + +import java.awt.event.ActionEvent; +import java.awt.event.WindowEvent; +import java.lang.ref.Reference; +import java.util.ArrayList; +import java.util.Objects; +import java.util.Random; +import java.util.Set; +import java.util.stream.Collectors; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.core.Main; +import de.uka.ilkd.key.gui.actions.EditMostRecentFileAction; +import de.uka.ilkd.key.gui.actions.KeYProjectHomepageAction; +import de.uka.ilkd.key.gui.actions.LemmaGenerationAction; +import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +import org.key_project.util.java.SwingUtil; + +import bibliothek.gui.dock.dockable.AbstractDockable; +import org.junit.jupiter.api.*; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Random testing of the UI. Will click random buttons and perform random actions. + * + * @author Arne Keller + */ +final class ChaosMonkey { + + private static final Logger LOGGER = LoggerFactory.getLogger(ChaosMonkey.class); + + private static final Set BANNED_ACTIONS = + Set.of("Open the last opened file with the default external editor", "Show log"); + private static final Set> BANNED_KEY_ACTIONS = + Set.of(LemmaGenerationAction.ProveKeYTaclets.class, + KeYProjectHomepageAction.class, + EditMostRecentFileAction.class, + LogView.OpenLogExternalAction.class); + /** + * Actions that should not be done, specified by class name. + * Use this if the action is a private class! + */ + private static final Set BANNED_KEY_ACTIONS_BY_CLASS_NAME = Set.of( + "de.uka.ilkd.key.gui.help.HelpFacade$OpenHelpAction"); + + private static boolean detectedError = false; + + @Test + @Disabled + void clickAllTheButtons() { + new Thread(ChaosMonkey::click, "ChaosMonkey").start(); + + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() + .setShowLoadExamplesDialog(false); + + Main.main( + "--examples ../key.ui/examples ../key.ui/examples/firstTouch/01-Agatha/project.key" + .split(" ")); + MainWindow mw = MainWindow.getInstance(); + mw.setSize(800, 600); + mw.setLocation(0, 0); + + try { + while (true) { + Thread.sleep(100000); + } + } catch (InterruptedException e) { + } + } + + static void click() { + // wishlist: + // - interaction with dialogs/popup menus besides closing them + try { + Thread.sleep(3000); + } catch (InterruptedException e) { + return; + } + MainWindow mw = MainWindow.getInstance(); + KeYMediator mediator = mw.getMediator(); + Random rand = new Random(); + try { + while (!detectedError) { + // wait for automode to finish + mediator.getUI().getProofControl().waitWhileAutoMode(); + + // close any dialogs and popup menus + var windows = SwingUtil.getAllOpenWindows(); + for (var window : windows) { + if (window instanceof MainWindow || !window.isVisible()) { + continue; + } + String title = window instanceof JDialog ? ((JDialog) window).getTitle() + : window.getClass().toString(); + LOGGER.info("closing: {}", title); + SwingUtilities.invokeLater(() -> { + window.dispatchEvent(new WindowEvent(window, WindowEvent.WINDOW_CLOSING)); + }); + Thread.sleep(500); + } + var popups = SwingUtil.getPopups(); + for (var popup : popups) { + LOGGER.info("hiding popup menu"); + popup.setVisible(false); + Thread.sleep(250); + } + + // now, find a random button to press >:) + var buttons = SwingUtil.findAllComponents(MainWindow.getInstance(), JButton.class); + var keyActions = KeyStrokeManager.getAllActions() + .stream().map(Reference::get).filter(Objects::nonNull) + .collect(Collectors.toSet()); + var allMenuItems = + SwingUtil.findAllComponents(MainWindow.getInstance(), JMenuItem.class); + var actions = new ArrayList<>(); + actions.addAll(buttons); + actions.addAll(keyActions); + for (var menuItem : allMenuItems) { + if (menuItem.getAction() != null && keyActions.contains(menuItem.getAction())) { + continue; + } + if (!menuItem.isEnabled() || (menuItem instanceof JMenu)) { + continue; + } + actions.add(menuItem); + } + var foundButton = false; + LOGGER.info("monkey chooses from {} buttons, actions and menu items ...", + actions.size()); + for (int i = 0; i < 100; i++) { + int actionIdx = rand.nextInt(actions.size()); + var action = actions.get(actionIdx); + if (action instanceof JButton) { + JButton button = (JButton) action; + // only enabled buttons + // (the "Show log" button is broken in test cases) + if (!button.isEnabled() || (button.getToolTipText() != null + && BANNED_ACTIONS.contains(button.getToolTipText()))) { + continue; + } + LOGGER.info("monkey clicks on {} {} {}", button.getClass(), + button.getName(), button.getToolTipText()); + var hierarchy = new ArrayList<>(); + var container = button.getParent(); + while (container != null) { + hierarchy.add(container); + container = container.getParent(); + } + for (var x : hierarchy) { + if (x instanceof AbstractDockable) { + AbstractDockable c = (AbstractDockable) x; + LOGGER.info(" {}", c.getTitleText()); + } else { + LOGGER.info(" {}", x); + } + } + SwingUtilities.invokeLater(() -> { + try { + button.doClick(); + } catch (Exception e) { + LOGGER.error("detected uncaught exception ", e); + detectedError = true; + } + }); + foundButton = true; + break; + } else if (action instanceof Action) { + Action keyAction = (Action) action; + if (!keyAction.isEnabled() + || BANNED_KEY_ACTIONS.contains(keyAction.getClass()) + || BANNED_KEY_ACTIONS_BY_CLASS_NAME + .contains(keyAction.getClass().getName())) { + continue; + } + LOGGER.info("performing action {}", keyAction); + SwingUtilities.invokeLater(() -> { + try { + Object source = keyAction; + var menuItems = SwingUtil.findAllComponents(mw, JMenuItem.class); + for (var menuItem : menuItems) { + if (menuItem.getAction() == keyAction) { + source = menuItem; + break; + } + } + keyAction.actionPerformed(new ActionEvent(source, 0, "")); + } catch (Exception e) { + LOGGER.error("detected uncaught exception ", e); + detectedError = true; + } + }); + foundButton = true; + break; + } else if (action instanceof JMenuItem) { + var menuItem = (JMenuItem) action; + LOGGER.info("performing menu item {}", menuItem.getText()); + SwingUtilities.invokeLater(() -> { + try { + menuItem.doClick(50); + } catch (Exception e) { + LOGGER.error("detected uncaught exception ", e); + detectedError = true; + } + }); + foundButton = true; + break; + } + } + if (!foundButton) { + LOGGER.error("chaos monkey failed to find an enabled button!"); + break; + } + Thread.sleep(1000); + } + } catch (Exception e) { + LOGGER.error("chaos monkey failed (in unexpected way)! ", e); + } + } +} diff --git a/key.ui/src/test/resources/logback.xml b/key.ui/src/test/resources/logback.xml index 875e9e091de..eefd443474d 100644 --- a/key.ui/src/test/resources/logback.xml +++ b/key.ui/src/test/resources/logback.xml @@ -4,11 +4,11 @@ key.log false - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{short}%n + %-10relative %-5level %-15thread %-25logger{5} %msg %ex%n - \ No newline at end of file + diff --git a/key.util/src/main/java/org/key_project/util/java/SwingUtil.java b/key.util/src/main/java/org/key_project/util/java/SwingUtil.java deleted file mode 100644 index 8e2c3560782..00000000000 --- a/key.util/src/main/java/org/key_project/util/java/SwingUtil.java +++ /dev/null @@ -1,57 +0,0 @@ -package org.key_project.util.java; - -import java.awt.*; -import javax.swing.*; - -/** - * Utilities for working with Swing. - * - * @author Arne Keller - */ -public final class SwingUtil { - private SwingUtil() { - } - - /** - * Find a component of the specified class in the container. - * This will search recursively. - * - * @param container container to search in - * @param classToFind class to look for - * @return the object if found, otherwise null - * @param class of the component - */ - public static T findComponent(Container container, Class classToFind) { - for (int i = 0; i < container.getComponentCount(); i++) { - var c = container.getComponent(i); - if (c.getClass().equals(classToFind)) { - return (T) c; - } else if (c instanceof Container) { - var f = findComponent((Container) c, classToFind); - if (f != null) { - return f; - } - } - } - return null; - } - - /** - * Create a scroll pane around the given table. - * It will always have vertical and horizontal scroll bars. - * - * @param table the table - * @return the scroll pane - */ - public static JScrollPane createScrollPane(JTable table) { - var scrollPane = new JScrollPane(table, ScrollPaneConstants.VERTICAL_SCROLLBAR_ALWAYS, - ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS); - - Dimension dim = new Dimension(table.getPreferredSize()); - dim.width += (Integer) UIManager.get("ScrollBar.width") + 2; - dim.height = scrollPane.getPreferredSize().height; - scrollPane.setPreferredSize(dim); - - return scrollPane; - } -} diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java index 8ff28d48f4f..c2417b013e5 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java @@ -24,8 +24,12 @@ import de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator; import de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + public class CounterExampleAction extends MainWindowAction { private static final long serialVersionUID = -1931682474791981751L; + private static final Logger LOGGER = LoggerFactory.getLogger(CounterExampleAction.class); private static final String NAME = "Search for Counterexample"; private static final String TOOLTIP = "Search for a counterexample for the selected goal"; @@ -106,6 +110,7 @@ public void actionPerformed(ActionEvent e) { getMediator().addInterruptedListener(worker); worker.execute(); } catch (Exception exc) { + LOGGER.error("", exc); IssueDialog.showExceptionDialog(mainWindow, exc); } } diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java index 245ad756352..d9d9d0d11f8 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java @@ -100,7 +100,6 @@ public TGInfoDialog(Window owner) { setTitle("Test Suite Generation"); setSize(1000, 700); setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); - setLocationRelativeTo(MainWindow.getInstance()); setLayout(new BorderLayout()); final JScrollPane scrollpane = new JScrollPane(textArea); diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java index fc2464b6693..24d2d3bef44 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java @@ -39,6 +39,7 @@ public TestGenerationAction(MainWindow mainWindow) { public void actionPerformed(ActionEvent e) { TGInfoDialog dlg = new TGInfoDialog(mainWindow); dlg.setVisible(true); + dlg.setLocationRelativeTo(mainWindow); }