Show notification after running macro (#3269)

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)

Author: unp1

key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java

@@ -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());
     }
 
@@ -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,
@@ -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) {
@@ -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();
@@ -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);
     }
 }

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<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) {

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

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
@@ -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,

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<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
      */
@@ -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");
+        }
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -1237,6 +1237,7 @@ public void scrollTo(int y) {
     }
 
     void displayResults(String message) {
+        LOGGER.debug("displaying results: {}", message);
         setStatusLine(message);
     }
 

key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java

@@ -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.

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

@@ -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;
@@ -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;
@@ -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;
@@ -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) {
@@ -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 {
@@ -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)