Skip to content

Commit

Permalink
Show notification after running macro (KeYProject#3269)
Browse files Browse the repository at this point in the history 
This PR adds a notification that will show up after a macro is done.
Depending on the settings it will always / when the KeY window is not
focused / never show up.

|OS (Desktop Environment) |  |
| - | - |
| Windows |
![screenshot-notification-windows](https://github.com/KeYProject/key/assets/94171076/9fe5febc-5d32-4808-bb93-b3573f760fd4)
|
| MacOS |
![screenshot-notification-macos](https://github.com/KeYProject/key/assets/8257939/38707e48-2a84-4217-bf19-3079aac5e21d")
(claims it comes from the app "Script Editor") |
| Linux (KDE) |
![image](https://github.com/KeYProject/key/assets/12560461/6071fada-6bbb-4485-8b49-83311f5b73e2)
|
| Linux (Gnome) |
![screenshot-notification-gnome](https://github.com/KeYProject/key/assets/94171076/8ccc3bda-93d6-40b3-a448-0b841aa989b4)
|
| Linux (XFCE) |
![screenshot-notification-xfce](https://github.com/KeYProject/key/assets/94171076/2ffa6eff-9390-42ec-8299-4fa80be73dbc)
|
| Linux (Cinnamon) |
![screenshot-notification-cinnamon](https://github.com/KeYProject/key/assets/94171076/edb96e32-b8f9-4151-ac92-179d112711bd)
|

The view settings panel has also been restructured.

![Screenshot_20230922_090859](https://github.com/KeYProject/key/assets/12560461/865c2a72-9ac0-48a6-8f68-a58a7025beb4)
  • Loading branch information
@unp1
unp1 authored Nov 13, 2023
2 parents ae6efac + b7c549d commit e978aed
Show file tree
Hide file tree
Showing 11 changed files with 242 additions and 55 deletions.
38 changes: 13 additions & 25 deletions key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,36 +27,33 @@
public class ProofMacroFinishedInfo extends DefaultTaskFinishedInfo {

private final Map<String, Object> proofMacroSpecificData = new HashMap<>();
private final boolean cancelled;


ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> 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.<Goal>nil().prepend(goal), proof, time, appliedRules,
closedGoals, false);
closedGoals);
}

ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> 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 - 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()));
}

ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals, Proof proof,
boolean cancelled) {
ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals, Proof proof) {
this(macro, goals, proof, proof == null ? null : proof.getStatistics());
}

Expand All @@ -69,7 +66,7 @@ public ProofMacroFinishedInfo(ProofMacro macro, Goal goal) {
}

public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals) {
this(macro, goals, goals.isEmpty() ? null : goals.head().proof(), false);
this(macro, goals, goals.isEmpty() ? null : goals.head().proof());
}

public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals,
Expand All @@ -79,36 +76,31 @@ public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals,
}

public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) {
this(macro, proof.openEnabledGoals(), proof, false);
}

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<Goal> 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<Goal> 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) {
Expand All @@ -123,10 +115,6 @@ public ProofMacro getMacro() {
return (ProofMacro) getSource();
}

public boolean isCancelled() {
return cancelled;
}

@SuppressWarnings("unchecked")
public ImmutableList<Goal> getGoals() {
final Object result = getResult();
Expand All @@ -138,6 +126,6 @@ public ImmutableList<Goal> getGoals() {
}

public static ProofMacroFinishedInfo getDefaultInfo(ProofMacro macro, Proof proof) {
return new ProofMacroFinishedInfo(macro, ImmutableSLList.nil(), proof, false);
return new ProofMacroFinishedInfo(macro, ImmutableSLList.nil(), proof);
}
}
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
}
final ImmutableList<Goal> 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) {
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 4 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@

public class DefaultTaskFinishedInfo implements TaskFinishedInfo {

/**
* See {@link TaskFinishedInfo#getSource()} for possible values.
*/
private final Object source;

// TODO
Expand All @@ -27,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,
Expand Down
28 changes: 23 additions & 5 deletions key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down Expand Up @@ -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";
Expand Down Expand Up @@ -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
*/
Expand Down Expand Up @@ -215,6 +217,9 @@ public class ViewSettings extends AbstractPropertiesSettings {
private final PropertyEntry<List<String>> folderBookmarks =
createStringListProperty(USER_FOLDER_BOOKMARKS, System.getProperty("user.home"));

private final PropertyEntry<String> notificationAfterMacro =
createStringProperty(NOTIFICATION_AFTER_MACRO, NOTIFICATION_UNFOCUSED);

/**
* Clutter rules are rules with less priority in the taclet menu
*/
Expand Down Expand Up @@ -555,4 +560,17 @@ public List<String> getFolderBookmarks() {
public void setFolderBookmarks(List<String> 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");
}
}
}
1 change: 1 addition & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1237,6 +1237,7 @@ public void scrollTo(int y) {
}

void displayResults(String message) {
LOGGER.debug("displaying results: {}", message);
setStatusLine(message);
}

Expand Down
2 changes: 1 addition & 1 deletion key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,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.
Expand Down
32 changes: 29 additions & 3 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,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;
Expand All @@ -48,6 +50,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;
Expand Down Expand Up @@ -192,9 +195,12 @@ private void taskFinishedInternal(TaskFinishedInfo info) {
"Couldn't close Goal Nr. " + g.node().serialNr() + " automatically");
dialog.show();
}
if (!isAtLeastOneMacroRunning()) {
showNotification("Automated proof search", info.toString());
}
}
mainWindow.displayResults(info.toString());
} else if (info != null && info.getSource() instanceof ProofMacro) {
} else if (info != null && info.getSource() instanceof ProofMacro macro) {
if (!isAtLeastOneMacroRunning()) {
mainWindow.hideStatusProgress();
assert info instanceof ProofMacroFinishedInfo;
Expand All @@ -210,9 +216,12 @@ private void taskFinishedInternal(TaskFinishedInfo info) {
"Couldn't close Goal Nr. " + g.node().serialNr() + " automatically");
dialog.show();
}
if (!isAtLeastOneMacroRunning()) {
showNotification(macro.getName(), info.toString());
}
}
}
} 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) {
Expand All @@ -223,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<String, Location> scriptAndLoc;
try {
Expand All @@ -249,6 +257,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)
Expand Down
Loading

0 comments on commit e978aed

Please sign in to comment.