Show notification after running macro

[FliegendeWurst]

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
MacOS	(claims it comes from the app "Script Editor")
Linux (KDE)
Linux (Gnome)
Linux (XFCE)
Linux (Cinnamon)

The view settings panel has also been restructured.

[codecov]

Codecov Report

Merging #3269 (b7c549d) into main (ae6efac) will decrease coverage by 0.01%.
The diff coverage is 15.78%.

@@             Coverage Diff              @@
##               main    #3269      +/-   ##
============================================
- Coverage     37.84%   37.84%   -0.01%     
  Complexity    16895    16895              
============================================
  Files          2054     2054              
  Lines        125490   125494       +4     
  Branches      21227    21228       +1     
============================================
+ Hits          47495    47496       +1     
- Misses        72142    72145       +3     
  Partials       5853     5853              

Files	Coverage Δ
...ain/java/de/uka/ilkd/key/macros/TryCloseMacro.java	11.11% <ø> (ø)
.../ilkd/key/prover/impl/DefaultTaskFinishedInfo.java	26.66% <ø> (ø)
...a/de/uka/ilkd/key/macros/SequentialProofMacro.java	6.25% <0.00%> (ø)
...in/java/de/uka/ilkd/key/settings/ViewSettings.java	37.58% <25.00%> (-0.76%)	⬇️
...de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java	14.28% <10.00%> (-0.81%)	⬇️

📣 Codecov offers a browser extension for seamless coverage viewing on GitHub. Try it in Chrome or Firefox today!

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[FliegendeWurst]

I just tried this PR on Windows 10. For some reason the notification only appears in the notification center, not on the screen. Making this whole feature almost completely useless...

[WolframPfeifer]

I just tried this PR on Windows. For some reason the notification only appears in the notification center, not on the screen. Making this whole feature almost completely useless...

On my Windows 11 machine, it looks fine:

Two notes though:

• It would be better to show "KeY" instead of "OpenJDK Platform binary", but I think it is impossible with this API.
• The notification is shown in the notification center as long as it is displayed, afterwards is disappears from the notification center. This seems to be a recent bug in Windows (https://bugs.openjdk.org/browse/JDK-8315647).

[FliegendeWurst]

It would be better to show "KeY" instead of "OpenJDK Platform binary", but I think it is impossible with this API.

I have checked this out and it appears the only way is to remove that text completely. That is what I've done in my latest commit. It should still show the icon though.

Implement a MacOS version of the notification (maybe Richard @unp1 can test it).

The MacOS version is ready for testing now.

[WolframPfeifer]

I did some quick tests with different desktop environments. Seems to look fine everywhere. I added the screenshots in the PR description.

[WolframPfeifer]

@unp1 Could you please check that displaying a notification works on macOS? I think that nobody else has a Mac and can test it.

[unp1]

@unp1 Could you please check that displaying a notification works on macOS? I think that nobody else has a Mac and can test it.

Just checked it. The setting is on always, but notifications do show up. We can look at it together in/after the KeY meeting.

[unp1]

@unp1 Could you please check that displaying a notification works on macOS? I think that nobody else has a Mac and can test it.

Just checked it. The setting is on always, but notifications do show up. We can look at it together in/after the KeY meeting.

OK, first good news it works (it does not show a notification if the macro managed to close the proof, which makes sense).

One problem is that macOS thinks the notification comes from its ScriptEditor. This has two minor issues (1) the user thinks it comes from a different program and (2) if the ScriptEditor is not allowed to send notification, the user will not see them for KeY either.

In principle it seems to be possible (according to apples documentation) to pass an icon to osascript, but as there are several discussions that say it is not possible, I assume it has been added lately. I suggest we live with the Script Editor icon for the moment. Alternatively, the provided Java only alternative works as well with the following drawbacks:

1. it seems as one can only allow all or no Java application to send notification
2. the icon used is a rather ugly terminal/java icon.

[FliegendeWurst]

(1) the user thinks it comes from a different program

Almost the same problem applies to the Windows notification, which comes from the "OpenJDK Platform Binary". At least we can set the icon on Windows.

I have changed the default to "when KeY is not focused" as discussed.