Optimize UI updates of slicing panel

[FliegendeWurst]

Related Issue

This pull request resolves #3734.

Intended Change

• reduce UI update frequency of slicing panel to once every 500 ms
• reduce work done per rule application to the bare minimum

Alternative: add a listener that listens for macro finish and proof loaded events. Though I think we can afford updating the UI twice a second.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: UI still updates as expected
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

Thanks for the PR and fast response! However, in my opinion it would be better to have as little RuleAppListeners as possible, since that obviously is a per-rule overhead. Also, I think it would make sense to have MacroFinish and ProofLoaded events/listeners in any case.

[wadoon]

I thought the RuleAppListeners are disabled during the proof task. In general, we should rather put additional workload after the proof search.

In this case, the main workload is not to query the graph size of the slicing, rather to calculate the dependency at all.

[FliegendeWurst]

In the extension settings, there is an option "Always track dependencies". If it is not checked, the dependency graph will be created when needed later.

[WolframPfeifer]

I thought the RuleAppListeners are disabled during the proof task. In general, we should rather put additional workload after the proof search.

In this case, the main workload is not to query the graph size of the slicing, rather to calculate the dependency at all.

I don't think that the RuleAppListeners are disabled in auto mode. Therefore, I think my comment is still valid, and I would prefer to completely get rid of the RuleAppListener for performance reasons. Can we maybe implement the update of the GUI in selectedNodeChanged (without a timer)? On the other hand, this would also recalculate when just "scrolling" the proof, right? But probably still better than doing something (even if just starting/restarting a timer) with every rule application.

[WolframPfeifer]

In the extension settings, there is an option "Always track dependencies". If it is not checked, the dependency graph will be created when needed later.

Maybe this should be the default setting then? Also, I noticed that with this flag switched off, the "Dependency Graph" part in the Slicing panel always shows 0 nodes and edges, even after the analysis was run (so the graph for sure is present and non-empty).

[FliegendeWurst]

I now removed both RuleAppListeners. Not running the dependency tracker during the proof improves performance by 3-5%.

The UI updates should be fixed.