From 2a0c18860a0667725b26145ef461b8ba84ad5040 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 16 Aug 2023 14:36:29 +0200 Subject: [PATCH 1/7] Show notification after running macro --- .../key/macros/ProofMacroFinishedInfo.java | 36 ++++------ .../ilkd/key/macros/SequentialProofMacro.java | 2 +- .../ilkd/key/macros/StrategyProofMacro.java | 2 +- .../de/uka/ilkd/key/macros/TryCloseMacro.java | 2 +- .../key/gui/WindowUserInterfaceControl.java | 9 +++ .../org/key_project/util/java/SwingUtil.java | 65 +++++++++++++++++++ 6 files changed, 91 insertions(+), 25 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java index 921e5f47d39..616d045baa8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java @@ -25,36 +25,33 @@ public class ProofMacroFinishedInfo extends DefaultTaskFinishedInfo { private final Map proofMacroSpecificData = new HashMap<>(); - private final boolean cancelled; ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof, long time, - int appliedRules, int closedGoals, boolean cancelled) { + int appliedRules, int closedGoals) { super(macro, goals, proof, time, appliedRules, closedGoals); - this.cancelled = cancelled; } ProofMacroFinishedInfo(ProofMacro macro, Goal goal, Proof proof, long time, int appliedRules, int closedGoals) { this(macro, ImmutableSLList.nil().prepend(goal), proof, time, appliedRules, - closedGoals, false); + closedGoals); } ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof, Statistics statistics) { this(macro, goals, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.totalRuleApps, - proof == null ? 0 : (proof.countBranches() - proof.openGoals().size()), false); + statistics == null ? 0 : statistics.nodes, + proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } ProofMacroFinishedInfo(ProofMacro macro, Goal goal, Proof proof, Statistics statistics) { this(macro, goal, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.totalRuleApps, + statistics == null ? 0 : statistics.nodes, proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } - ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof, - boolean cancelled) { + ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof) { this(macro, goals, proof, proof == null ? null : proof.getStatistics()); } @@ -67,40 +64,39 @@ public ProofMacroFinishedInfo(ProofMacro macro, Goal goal) { } public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals) { - this(macro, goals, goals.isEmpty() ? null : goals.head().proof(), false); + this(macro, goals, goals.isEmpty() ? null : goals.head().proof()); } public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) { - this(macro, proof.openEnabledGoals(), proof, false); + this(macro, proof.openEnabledGoals(), proof); } public ProofMacroFinishedInfo(ProofMacro macro, Proof proof, boolean cancelled) { - this(macro, proof.openEnabledGoals(), proof, cancelled); + this(macro, proof.openEnabledGoals(), proof); } public ProofMacroFinishedInfo(ProofMacro macro, ProofMacroFinishedInfo info) { - this(macro, info.getGoals(), info.getProof(), info.cancelled); + this(macro, info.getGoals(), info.getProof()); } ProofMacroFinishedInfo(ProofMacro macro, ProofMacroFinishedInfo info, ImmutableList goals) { this(macro, goals, info.getProof(), info.getTime(), info.getAppliedRules(), - info.getClosedGoals(), info.cancelled); + info.getClosedGoals()); } ProofMacroFinishedInfo(ProofMacroFinishedInfo info, ApplyStrategyInfo stratInfo) { this(info.getMacro(), info.getGoals(), info.getProof(), info.getTime() + stratInfo.getTime(), info.getAppliedRules() + stratInfo.getAppliedRuleApps(), - info.getClosedGoals() + stratInfo.getClosedGoals(), info.cancelled); + info.getClosedGoals() + stratInfo.getClosedGoals()); } ProofMacroFinishedInfo(ProofMacroFinishedInfo info, ApplyStrategyInfo stratInfo, ImmutableList goals) { this(info.getMacro(), goals, stratInfo.getProof(), info.getTime() + stratInfo.getTime(), info.getAppliedRules() + stratInfo.getAppliedRuleApps(), - goals.size() <= info.getGoals().size() ? (info.getGoals().size() - goals.size()) : 0, - false); + goals.size() <= info.getGoals().size() ? (info.getGoals().size() - goals.size()) : 0); } public void addInfo(String key, Object value) { @@ -115,10 +111,6 @@ public ProofMacro getMacro() { return (ProofMacro) getSource(); } - public boolean isCancelled() { - return cancelled; - } - @SuppressWarnings("unchecked") public ImmutableList getGoals() { final Object result = getResult(); @@ -130,6 +122,6 @@ public ImmutableList getGoals() { } public static ProofMacroFinishedInfo getDefaultInfo(ProofMacro macro, Proof proof) { - return new ProofMacroFinishedInfo(macro, ImmutableSLList.nil(), proof, false); + return new ProofMacroFinishedInfo(macro, ImmutableSLList.nil(), proof); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java index 41c0265aec8..f0f1e32fa43 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java @@ -84,7 +84,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, } final ImmutableList gs = initNodes.isEmpty() ? proof.openEnabledGoals() : proof.getSubtreeEnabledGoals(initNodes.get(0)); - ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, gs, proof, false); + ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, gs, proof); for (final ProofMacro macro : getProofMacros()) { // reverse to original nodes for (Node initNode : initNodes) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java index fe275f66318..47af7b5ab20 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java @@ -99,7 +99,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, Strategy oldStrategy = proof.getActiveStrategy(); proof.setActiveStrategy(createStrategy(proof, posInOcc)); - ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals, proof, false); + ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals, proof); try { // find the relevant goals // and start diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java index e6b435383eb..0485a5d6464 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java @@ -162,7 +162,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, // // inform the listener ProofMacroFinishedInfo info = - new ProofMacroFinishedInfo(this, goals, proof, 0, 0, 0, false); + new ProofMacroFinishedInfo(this, goals, proof, 0, 0, 0); // // start actual autoprove 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 f4541f12a73..cdc24f172cc 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 @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; +import java.awt.*; import java.io.File; import java.io.IOException; import java.util.Collection; @@ -48,6 +49,7 @@ import de.uka.ilkd.key.util.ThreadUtilities; import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.java.SwingUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -178,9 +180,13 @@ private void taskFinishedInternal(TaskFinishedInfo info) { "Couldn't close Goal Nr. " + g.node().serialNr() + " automatically"); dialog.show(); } + if (!isAtLeastOneMacroRunning() && !MainWindow.getInstance().isActive()) { + SwingUtil.showNotification("Automated proof search", info.toString()); + } } mainWindow.displayResults(info.toString()); } else if (info != null && info.getSource() instanceof ProofMacro) { + ProofMacro macro = (ProofMacro) info.getSource(); if (!isAtLeastOneMacroRunning()) { resetStatus(this); assert info instanceof ProofMacroFinishedInfo; @@ -196,6 +202,9 @@ private void taskFinishedInternal(TaskFinishedInfo info) { "Couldn't close Goal Nr. " + g.node().serialNr() + " automatically"); dialog.show(); } + if (!isAtLeastOneMacroRunning() && !MainWindow.getInstance().isActive()) { + SwingUtil.showNotification(macro.getName(), info.toString()); + } } } } else if (info != null && info.getSource() instanceof ProblemLoader) { 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 index 02b789e01dd..13aee67b17a 100644 --- 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 @@ -5,6 +5,7 @@ import java.awt.*; +import java.io.IOException; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -13,7 +14,11 @@ import java.util.Set; import javax.swing.*; +import de.uka.ilkd.key.gui.fonticons.IconFactory; + import bibliothek.gui.dock.themes.basic.BasicDockableDisplayer; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * Utilities for working with Swing. @@ -21,6 +26,11 @@ * @author Arne Keller */ public final class SwingUtil { + public static final Logger LOGGER = LoggerFactory.getLogger(SwingUtil.class); + + private static boolean notifySendAvailable = false; + private static boolean notifySendChecked = false; + private SwingUtil() { } @@ -179,4 +189,59 @@ public static void setFont(JComponent component, Font font) { setFont(((JMenu) component).getPopupMenu(), font); } } + + /** + * Show a desktop notification to the user. + * + * @param title title of the notification + * @param text text of the notification + */ + public static void showNotification(String title, String text) { + // Linux: try notify-send first (looks better) + if (System.getProperty("os.name").equals("Linux")) { + if (!notifySendChecked) { + notifySendChecked = true; + notifySendAvailable = true; + try { + new ProcessBuilder( + "notify-send", + "-?").start().waitFor(); + } catch (IOException | InterruptedException e) { + LOGGER.warn("notify-send is not available (will not display notifications!)"); + notifySendAvailable = false; + } + } + if (!notifySendAvailable) { + // the default Swing notification on Linux looks hideous + // => do not notify! + return; + } + try { + new ProcessBuilder( + "notify-send", + "-a", "KeY", title, text).start().waitFor(); + } catch (IOException | InterruptedException e) { + // since we checked for notify-send previously, this error is unlikely + LOGGER.warn("failed to show notification ", e); + } + } else { + SystemTray tray = null; + TrayIcon trayIcon = null; + try { + tray = SystemTray.getSystemTray(); + + trayIcon = new TrayIcon(IconFactory.keyLogo(), "KeY"); + // Let the system resize the image if needed + trayIcon.setImageAutoSize(true); + tray.add(trayIcon); + trayIcon.displayMessage(title, text, TrayIcon.MessageType.INFO); + } catch (AWTException e) { + LOGGER.warn("failed to show notification ", e); + } finally { + if (tray != null && trayIcon != null) { + tray.remove(trayIcon); + } + } + } + } } From ccc5c38ff3949962db499680c30484301bbf3628 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 21 Sep 2023 10:00:36 +0200 Subject: [PATCH 2/7] Notifications: macOS implementation --- .../util/java/CheckedProcessBuilder.java | 74 +++++++++++++++++++ .../org/key_project/util/java/SwingUtil.java | 53 +++++++------ 2 files changed, 100 insertions(+), 27 deletions(-) create mode 100644 key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java diff --git a/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java b/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java new file mode 100644 index 00000000000..fa1b4a72e1d --- /dev/null +++ b/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java @@ -0,0 +1,74 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.util.java; + +import java.io.IOException; +import java.util.HashSet; +import java.util.Set; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Process builder that first checks whether a program is installed. + * + * @author Arne Keller + */ +public class CheckedProcessBuilder { + public static final Logger LOGGER = LoggerFactory.getLogger(CheckedProcessBuilder.class); + + /** + * The programs already checked. + */ + private static final Set CHECKED = new HashSet<>(); + /** + * Installed programs. + */ + private static final Set AVAILABLE = new HashSet<>(); + /** + * Program of this builder. + */ + private final String program; + + /** + * Create a new builder and check for the given program. + * + * @param program the program + * @param programCheck program invocation used to check (e.g. z3 --version) + */ + public CheckedProcessBuilder(String program, String[] programCheck) { + this.program = program; + if (CHECKED.contains(program)) { + return; + } + CHECKED.add(program); + try { + new ProcessBuilder(programCheck).start().waitFor(); + AVAILABLE.add(program); + } catch (IOException | InterruptedException e) { + // not available + LOGGER.warn("{} is not available", program); + } + } + + /** + * Start and wait for the program with the given argument list. + * If the program is not available, no action is done. + * + * @param args arguments + * @throws IOException on start error (unlikely) + * @throws InterruptedException on wait error + */ + public void start(String... args) throws IOException, InterruptedException { + if (args.length == 0) { + throw new IllegalStateException("need program to execute"); + } + if (!args[0].equals(program)) { + throw new IllegalStateException("used for wrong program"); + } + if (AVAILABLE.contains(program)) { + new ProcessBuilder(args).start().waitFor(); + } + } +} 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 index 13aee67b17a..b901c763f14 100644 --- 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 @@ -27,9 +27,8 @@ */ public final class SwingUtil { public static final Logger LOGGER = LoggerFactory.getLogger(SwingUtil.class); + private static final String NOTIFICATION_ERROR = "failed to show notification "; - private static boolean notifySendAvailable = false; - private static boolean notifySendChecked = false; private SwingUtil() { } @@ -197,46 +196,46 @@ public static void setFont(JComponent component, Font font) { * @param text text of the notification */ public static void showNotification(String title, String text) { - // Linux: try notify-send first (looks better) - if (System.getProperty("os.name").equals("Linux")) { - if (!notifySendChecked) { - notifySendChecked = true; - notifySendAvailable = true; - try { - new ProcessBuilder( - "notify-send", - "-?").start().waitFor(); - } catch (IOException | InterruptedException e) { - LOGGER.warn("notify-send is not available (will not display notifications!)"); - notifySendAvailable = false; - } - } - if (!notifySendAvailable) { - // the default Swing notification on Linux looks hideous - // => do not notify! - return; - } + if (System.getProperty("os.name").startsWith("Linux")) { + // Linux: try notify-send (looks better than SystemTray) + String exe = "notify-send"; try { - new ProcessBuilder( - "notify-send", - "-a", "KeY", title, text).start().waitFor(); + new CheckedProcessBuilder(exe, new String[] { exe, "-?" }) + .start(exe, "-a", "KeY", title, text); } catch (IOException | InterruptedException e) { // since we checked for notify-send previously, this error is unlikely - LOGGER.warn("failed to show notification ", e); + LOGGER.warn(NOTIFICATION_ERROR, e); + } + } else if (System.getProperty("os.name").startsWith("Mac")) { + // macOS: show a native notification + String exe = "osascript"; + try { + new CheckedProcessBuilder(exe, new String[] { exe, "-e", "return \"\"" }) + .start(exe, "-e", + "display notification \"%s\" with title \"%s\"".formatted(text, title)); + } catch (IOException | InterruptedException e) { + // since we checked for osascript previously, this error is unlikely + LOGGER.warn(NOTIFICATION_ERROR, e); } } else { + // else: use the Java API + // this will show a native notification on Windows 10/11 at least SystemTray tray = null; TrayIcon trayIcon = null; try { tray = SystemTray.getSystemTray(); + if (tray == null) { + LOGGER.warn(NOTIFICATION_ERROR + "(tray null)"); + return; + } trayIcon = new TrayIcon(IconFactory.keyLogo(), "KeY"); // Let the system resize the image if needed trayIcon.setImageAutoSize(true); tray.add(trayIcon); - trayIcon.displayMessage(title, text, TrayIcon.MessageType.INFO); + trayIcon.displayMessage(title, text, TrayIcon.MessageType.NONE); } catch (AWTException e) { - LOGGER.warn("failed to show notification ", e); + LOGGER.warn(NOTIFICATION_ERROR, e); } finally { if (tray != null && trayIcon != null) { tray.remove(trayIcon); From dcdd100c883a0e3cecaea37ba71f64a79cfcc20d Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 22 Sep 2023 08:33:51 +0200 Subject: [PATCH 3/7] Revert task statistics to show total rule apps --- .../de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java | 8 ++------ .../uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java | 3 +++ .../main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java | 2 +- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java index 616d045baa8..85b84756b95 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java @@ -41,13 +41,13 @@ public class ProofMacroFinishedInfo extends DefaultTaskFinishedInfo { ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof, Statistics statistics) { this(macro, goals, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.nodes, + statistics == null ? 0 : statistics.totalRuleApps, proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } ProofMacroFinishedInfo(ProofMacro macro, Goal goal, Proof proof, Statistics statistics) { this(macro, goal, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.nodes, + statistics == null ? 0 : statistics.totalRuleApps, proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } @@ -71,10 +71,6 @@ public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) { this(macro, proof.openEnabledGoals(), proof); } - public ProofMacroFinishedInfo(ProofMacro macro, Proof proof, boolean cancelled) { - this(macro, proof.openEnabledGoals(), proof); - } - public ProofMacroFinishedInfo(ProofMacro macro, ProofMacroFinishedInfo info) { this(macro, info.getGoals(), info.getProof()); } 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 10d0cda4960..4a861930bc8 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 @@ -8,6 +8,9 @@ public class DefaultTaskFinishedInfo implements TaskFinishedInfo { + /** + * See {@link TaskFinishedInfo#getSource()} for possible values. + */ private final Object source; // TODO 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 cca7480c1b7..c387f537f69 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 @@ -99,7 +99,7 @@ protected ProofMacroFinishedInfo doInBackground() { } } catch (final InterruptedException exception) { LOGGER.debug("Proof macro has been interrupted:", exception); - info = new ProofMacroFinishedInfo(macro, selectedProof, true); + info = new ProofMacroFinishedInfo(macro, selectedProof); this.exception = exception; } catch (final Exception exception) { // This should actually never happen. From 694609ab7be6e14e2d9a59b6268eb7833a9d2b9b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 22 Sep 2023 09:08:19 +0200 Subject: [PATCH 4/7] Notification after macro: add option --- .../uka/ilkd/key/settings/ViewSettings.java | 28 +++++++++-- .../key/gui/WindowUserInterfaceControl.java | 29 +++++++++-- .../key/gui/settings/StandardUISettings.java | 48 ++++++++++++------- .../util/java/CheckedProcessBuilder.java | 17 ++++--- .../org/key_project/util/java/SwingUtil.java | 10 ++-- 5 files changed, 91 insertions(+), 41 deletions(-) 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 1c912d4dea9..ce631ebfe43 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 @@ -13,6 +13,7 @@ * number is exceeded no SchemaVariables get instantiated in the displayed tooltip. 3) whether * intermediate proofsteps should be hidden in the proof tree view * + * @see de.uka.ilkd.key.gui.settings.StandardUISettings * @author unknown * @author weigl */ @@ -99,11 +100,6 @@ public class ViewSettings extends AbstractPropertiesSettings { */ private static final String CONFIRM_EXIT = "[View]ConfirmExit"; - /** - * Heatmap options property - */ - private static final String HEATMAP_OPTIONS = "[View]HeatmapOptions"; - private static final String FONT_SIZE_FACTOR = "[View]uiFontSizeFactor"; private static final String SEQUENT_VIEW_TOOLTIP = "[View]SequentViewTooltips"; @@ -145,9 +141,15 @@ public class ViewSettings extends AbstractPropertiesSettings { */ private static final String USER_FOLDER_BOOKMARKS = "[View]folderBookmarks"; + private static final String NOTIFICATION_AFTER_MACRO = "[View]notificationAfterMacro"; + private static final String LOOK_AND_FEEL_DEFAULT = UIManager.getCrossPlatformLookAndFeelClassName(); + public static final String NOTIFICATION_ALWAYS = "Always"; + public static final String NOTIFICATION_UNFOCUSED = "When not focused"; + public static final String NOTIFICATION_NEVER = "Never"; + /** * Show Taclet uninstantiated in tooltip -- for learning */ @@ -215,6 +217,9 @@ public class ViewSettings extends AbstractPropertiesSettings { private final PropertyEntry> folderBookmarks = createStringListProperty(USER_FOLDER_BOOKMARKS, System.getProperty("user.home")); + private final PropertyEntry notificationAfterMacro = + createStringProperty(NOTIFICATION_AFTER_MACRO, NOTIFICATION_ALWAYS); + /** * Clutter rules are rules with less priority in the taclet menu */ @@ -555,4 +560,17 @@ public List getFolderBookmarks() { public void setFolderBookmarks(List bm) { folderBookmarks.set(bm); } + + public String notificationAfterMacro() { + return notificationAfterMacro.get(); + } + + public void setNotificationAfterMacro(String value) { + if (value.equals(NOTIFICATION_ALWAYS) || value.equals(NOTIFICATION_UNFOCUSED) + || value.equals(NOTIFICATION_NEVER)) { + notificationAfterMacro.set(value); + } else { + throw new IllegalStateException("tried to set wrong value for notification setting"); + } + } } 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 cdc24f172cc..68d952dc67c 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 @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.awt.*; import java.io.File; import java.io.IOException; import java.util.Collection; @@ -39,6 +38,8 @@ import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.ViewSettings; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; @@ -180,8 +181,8 @@ private void taskFinishedInternal(TaskFinishedInfo info) { "Couldn't close Goal Nr. " + g.node().serialNr() + " automatically"); dialog.show(); } - if (!isAtLeastOneMacroRunning() && !MainWindow.getInstance().isActive()) { - SwingUtil.showNotification("Automated proof search", info.toString()); + if (!isAtLeastOneMacroRunning()) { + showNotification("Automated proof search", info.toString()); } } mainWindow.displayResults(info.toString()); @@ -202,8 +203,8 @@ private void taskFinishedInternal(TaskFinishedInfo info) { "Couldn't close Goal Nr. " + g.node().serialNr() + " automatically"); dialog.show(); } - if (!isAtLeastOneMacroRunning() && !MainWindow.getInstance().isActive()) { - SwingUtil.showNotification(macro.getName(), info.toString()); + if (!isAtLeastOneMacroRunning()) { + showNotification(macro.getName(), info.toString()); } } } @@ -244,6 +245,24 @@ private void taskFinishedInternal(TaskFinishedInfo info) { Runtime.getRuntime().gc(); } + /** + * Show a notification, if enabled by the settings. + * + * @param title header + * @param text body + */ + private void showNotification(String title, String text) { + var mode = + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().notificationAfterMacro(); + if (mode.equals(ViewSettings.NOTIFICATION_ALWAYS)) { + SwingUtil.showNotification(title, text); + } else if (mode.equals(ViewSettings.NOTIFICATION_UNFOCUSED)) { + if (!MainWindow.getInstance().isActive()) { + SwingUtil.showNotification(title, text); + } + } + } + protected boolean inStopAtFirstUncloseableGoalMode(Proof proof) { return proof.getSettings().getStrategySettings().getActiveStrategyProperties() .getProperty(StrategyProperties.STOPMODE_OPTIONS_KEY) 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 2df0719111b..e08e3da056d 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 @@ -57,6 +57,7 @@ public class StandardUISettings extends SettingsPanel implements SettingsProvide private final JCheckBox chkEnsureSourceConsistency; private final JTextArea txtClutterRules; private final JTextArea txtClutterRuleSets; + private final JComboBox notificationAfterMacro; public StandardUISettings() { setHeaderText(getDescription()); @@ -71,33 +72,52 @@ public StandardUISettings() { } } + addSeparator("General"); lookAndFeel = createSelection(LAF_LABELS.toArray(new String[0]), emptyValidator()); - addTitledComponent("Look and feel: ", lookAndFeel, LOOK_AND_FEEL_INFO); + addTitledComponent("Look and feel", lookAndFeel, LOOK_AND_FEEL_INFO); spFontSizeGlobal = createNumberTextField(new SpinnerNumberModel(1, 0.1, 5, 0.1), emptyValidator()); - addTitledComponent("Global font factor: ", spFontSizeGlobal, ""); + addTitledComponent("Global font factor", spFontSizeGlobal, ""); String[] sizes = Arrays.stream(Config.SIZES).boxed().map(it -> it + " pt").toArray(String[]::new); spFontSizeTreeSequent = this.createSelection(sizes, emptyValidator()); - addTitledComponent("Tree and sequent font factor: ", spFontSizeTreeSequent, ""); + addTitledComponent("Tree and sequent font size", spFontSizeTreeSequent, ""); String info = """ Maximum size (line count) of the tooltips of applicable rules -
with schema variable instantiations displayed. - In case of longer
tooltips the instantiation will be suppressed. + with schema variable instantiations displayed. + In case of longer tooltips the instantiation will be suppressed. """; txtMaxTooltipLines = addNumberField("Maximum line number for tooltips", 1, 100, 5, info, emptyValidator()); - chkShowLoadExamplesDialog = addCheckBox("Show load examples dialog", - "Show the load example dialog on startup", true, emptyValidator()); + chkShowLoadExamplesDialog = + addCheckBox("Show load examples dialog on startup", "", true, emptyValidator()); + chkConfirmExit = addCheckBox("Confirm program exit", "", false, emptyValidator()); + + spAutoSaveProof = + addNumberField("Auto save proof", 0, 10000000, 1000, "", emptyValidator()); + notificationAfterMacro = addComboBox("Notification after macro finished", "", 0, + emptyValidator(), ViewSettings.NOTIFICATION_ALWAYS, ViewSettings.NOTIFICATION_UNFOCUSED, + ViewSettings.NOTIFICATION_NEVER); + + addSeparator("Sequent View"); + chkPrettyPrint = addCheckBox("Pretty print terms", "", false, emptyValidator()); + chkUseUnicode = addCheckBox("Use unicode", "", false, emptyValidator()); + chkSyntaxHighlightning = + addCheckBox("Use syntax highlighting", "", false, emptyValidator()); + chkHidePackagePrefix = addCheckBox("Hide package prefix", "", false, emptyValidator()); + chkRightClickMacros = + addCheckBox("Right click for proof macros", "", false, emptyValidator()); + + addSeparator("Interaction"); chkShowWholeTacletCB = addCheckBox("Show whole taclet", - "Pretty-print whole Taclet including \n" + "'name', 'find', 'varCond' and 'heuristics'", + "Pretty-print whole Taclet including 'name', 'find', 'varCond' and 'heuristics'\n(applies to tooltips in context menu)", false, emptyValidator()); chkShowUninstantiatedTaclet = addCheckBox("Show uninstantiated taclet", @@ -108,20 +128,10 @@ Maximum size (line count) of the tooltips of applicable rules txtClutterRuleSets = addTextArea("Clutter Rulesets", "", INFO_CLUTTER_RULESET, emptyValidator()); - chkPrettyPrint = addCheckBox("Pretty print terms", "", false, emptyValidator()); - chkUseUnicode = addCheckBox("Use unicode", "", false, emptyValidator()); - chkSyntaxHighlightning = - addCheckBox("Use syntax highlighting", "", false, emptyValidator()); - chkHidePackagePrefix = addCheckBox("Hide package prefix", "", false, emptyValidator()); - chkConfirmExit = addCheckBox("Confirm program exit", "", false, emptyValidator()); - spAutoSaveProof = - addNumberField("Auto save proof", 0, 10000000, 1000, "", emptyValidator()); chkMinimizeInteraction = addCheckBox("Minimise interactions", MinimizeInteraction.TOOL_TIP, false, emptyValidator()); chkEnsureSourceConsistency = addCheckBox("Ensure source consistency", "", true, emptyValidator()); - chkRightClickMacros = - addCheckBox("Right click for proof macros", "", false, emptyValidator()); } @@ -161,6 +171,7 @@ public JComponent getPanel(MainWindow window) { spAutoSaveProof.setValue(generalSettings.autoSavePeriod()); chkMinimizeInteraction.setSelected(generalSettings.getTacletFilter()); spFontSizeTreeSequent.setSelectedIndex(vs.sizeIndex()); + notificationAfterMacro.setSelectedItem(vs.notificationAfterMacro()); return this; } @@ -195,6 +206,7 @@ public void applySettings(MainWindow window) throws InvalidSettingsInputExceptio gs.setAutoSave((Integer) spAutoSaveProof.getValue()); gs.setTacletFilter(chkMinimizeInteraction.isSelected()); vs.setFontIndex(spFontSizeTreeSequent.getSelectedIndex()); + vs.setNotificationAfterMacro((String) notificationAfterMacro.getSelectedItem()); Config.DEFAULT.setDefaultFonts(); FontSizeFacade.resizeFonts(vs.getUIFontSizeFactor()); Config.DEFAULT.fireConfigChange(); diff --git a/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java b/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java index fa1b4a72e1d..08b37eec378 100644 --- a/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java +++ b/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java @@ -4,8 +4,10 @@ package org.key_project.util.java; import java.io.IOException; +import java.util.Arrays; import java.util.HashSet; import java.util.Set; +import java.util.stream.Stream; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -35,7 +37,7 @@ public class CheckedProcessBuilder { * Create a new builder and check for the given program. * * @param program the program - * @param programCheck program invocation used to check (e.g. z3 --version) + * @param programCheck program invocation used to check (e.g. --version) */ public CheckedProcessBuilder(String program, String[] programCheck) { this.program = program; @@ -44,7 +46,9 @@ public CheckedProcessBuilder(String program, String[] programCheck) { } CHECKED.add(program); try { - new ProcessBuilder(programCheck).start().waitFor(); + String[] check = Stream.concat(Stream.of(program), Arrays.stream(programCheck)) + .toArray(String[]::new); + new ProcessBuilder(check).start().waitFor(); AVAILABLE.add(program); } catch (IOException | InterruptedException e) { // not available @@ -56,7 +60,7 @@ public CheckedProcessBuilder(String program, String[] programCheck) { * Start and wait for the program with the given argument list. * If the program is not available, no action is done. * - * @param args arguments + * @param args arguments (without program name) * @throws IOException on start error (unlikely) * @throws InterruptedException on wait error */ @@ -64,11 +68,10 @@ public void start(String... args) throws IOException, InterruptedException { if (args.length == 0) { throw new IllegalStateException("need program to execute"); } - if (!args[0].equals(program)) { - throw new IllegalStateException("used for wrong program"); - } if (AVAILABLE.contains(program)) { - new ProcessBuilder(args).start().waitFor(); + String[] fullArgs = + Stream.concat(Stream.of(program), Arrays.stream(args)).toArray(String[]::new); + new ProcessBuilder(fullArgs).start().waitFor(); } } } 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 index b901c763f14..4fe1f1a4453 100644 --- 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 @@ -198,20 +198,18 @@ public static void setFont(JComponent component, Font font) { public static void showNotification(String title, String text) { if (System.getProperty("os.name").startsWith("Linux")) { // Linux: try notify-send (looks better than SystemTray) - String exe = "notify-send"; try { - new CheckedProcessBuilder(exe, new String[] { exe, "-?" }) - .start(exe, "-a", "KeY", title, text); + new CheckedProcessBuilder("notify-send", new String[] { "-?" }) + .start("-a", "KeY", title, text); } catch (IOException | InterruptedException e) { // since we checked for notify-send previously, this error is unlikely LOGGER.warn(NOTIFICATION_ERROR, e); } } else if (System.getProperty("os.name").startsWith("Mac")) { // macOS: show a native notification - String exe = "osascript"; try { - new CheckedProcessBuilder(exe, new String[] { exe, "-e", "return \"\"" }) - .start(exe, "-e", + new CheckedProcessBuilder("osascript", new String[] { "-e", "return \"\"" }) + .start("-e", "display notification \"%s\" with title \"%s\"".formatted(text, title)); } catch (IOException | InterruptedException e) { // since we checked for osascript previously, this error is unlikely From 5e4ea4f0112ea8c7f41de351a7a7fce7a3dc3700 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 30 Oct 2023 18:13:16 +0100 Subject: [PATCH 5/7] Fix inconsistency with status bar --- .../java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java | 4 ++-- .../de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java | 2 +- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 1 + 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java index 0e419ab3139..962228f3ca8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java @@ -43,13 +43,13 @@ public class ProofMacroFinishedInfo extends DefaultTaskFinishedInfo { ProofMacroFinishedInfo(ProofMacro macro, ImmutableList goals, Proof proof, Statistics statistics) { this(macro, goals, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.totalRuleApps, + statistics == null ? 0 : statistics.nodes - statistics.branches, proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } ProofMacroFinishedInfo(ProofMacro macro, Goal goal, Proof proof, Statistics statistics) { this(macro, goal, proof, statistics == null ? 0 : statistics.timeInMillis, - statistics == null ? 0 : statistics.totalRuleApps, + statistics == null ? 0 : statistics.nodes - statistics.branches, proof == null ? 0 : (proof.countBranches() - proof.openGoals().size())); } 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 4a861930bc8..5681b0cda23 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 @@ -30,7 +30,7 @@ public class DefaultTaskFinishedInfo implements TaskFinishedInfo { * @param result task result * @param proof the proof the task worked on * @param time time the task took (milliseconds) - * @param appliedRules how many rules were applied + * @param appliedRules how many nodes were created * @param closedGoals how many goals were closed */ public DefaultTaskFinishedInfo(Object source, Object result, Proof proof, long time, 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 0dbd4fc5331..e86f23c5664 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 @@ -1232,6 +1232,7 @@ public void scrollTo(int y) { } void displayResults(String message) { + LOGGER.debug("displaying results: {}", message); setStatusLine(message); } From 98b3b55e624f57d331cba67dbe2186dea7a126d1 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 11 Nov 2023 12:21:10 +0100 Subject: [PATCH 6/7] Change default notification setting to unfocused --- .../src/main/java/de/uka/ilkd/key/settings/ViewSettings.java | 2 +- .../java/de/uka/ilkd/key/gui/settings/StandardUISettings.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 ec58737e9a7..8b7a850e692 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 @@ -218,7 +218,7 @@ public class ViewSettings extends AbstractPropertiesSettings { createStringListProperty(USER_FOLDER_BOOKMARKS, System.getProperty("user.home")); private final PropertyEntry notificationAfterMacro = - createStringProperty(NOTIFICATION_AFTER_MACRO, NOTIFICATION_ALWAYS); + createStringProperty(NOTIFICATION_AFTER_MACRO, NOTIFICATION_UNFOCUSED); /** * Clutter rules are rules with less priority in the taclet menu 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 e08e3da056d..f523c45e3bf 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 @@ -102,7 +102,7 @@ Maximum size (line count) of the tooltips of applicable rules spAutoSaveProof = addNumberField("Auto save proof", 0, 10000000, 1000, "", emptyValidator()); - notificationAfterMacro = addComboBox("Notification after macro finished", "", 0, + notificationAfterMacro = addComboBox("Notification after macro finished", "", 1, emptyValidator(), ViewSettings.NOTIFICATION_ALWAYS, ViewSettings.NOTIFICATION_UNFOCUSED, ViewSettings.NOTIFICATION_NEVER); From b7c549d575dcfa64fa8ecbb2cc5c3e21b83f0388 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 11 Nov 2023 12:22:21 +0100 Subject: [PATCH 7/7] Use pattern matching to avoid cast --- .../de/uka/ilkd/key/gui/WindowUserInterfaceControl.java | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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 d92626b3971..88d8f7c46ba 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 @@ -200,8 +200,7 @@ private void taskFinishedInternal(TaskFinishedInfo info) { } } mainWindow.displayResults(info.toString()); - } else if (info != null && info.getSource() instanceof ProofMacro) { - ProofMacro macro = (ProofMacro) info.getSource(); + } else if (info != null && info.getSource() instanceof ProofMacro macro) { if (!isAtLeastOneMacroRunning()) { mainWindow.hideStatusProgress(); assert info instanceof ProofMacroFinishedInfo; @@ -222,7 +221,7 @@ private void taskFinishedInternal(TaskFinishedInfo info) { } } } - } else if (info != null && info.getSource() instanceof ProblemLoader) { + } else if (info != null && info.getSource() instanceof ProblemLoader problemLoader) { resetStatus(this); Throwable result = (Throwable) info.getResult(); if (info.getResult() != null) { @@ -233,7 +232,6 @@ private void taskFinishedInternal(TaskFinishedInfo info) { } else { KeYMediator mediator = mainWindow.getMediator(); mediator.getNotationInfo().refresh(mediator.getServices()); - ProblemLoader problemLoader = (ProblemLoader) info.getSource(); if (problemLoader.hasProofScript()) { Pair scriptAndLoc; try {