diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 94d41fdd26d..9c63eafbdc4 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -132,7 +132,7 @@ private void createTrackerForProof(Proof newProof) { proof.addProofDisposedListener(this); DependencyTracker tracker = new DependencyTracker(proof); if (leftPanel != null) { - proof.addRuleAppListener(e -> leftPanel.ruleAppliedOnProof(proof, tracker)); + proof.addRuleAppListener(e -> leftPanel.ruleAppliedOnProof(proof)); proof.addProofTreeListener(leftPanel); if (enableSafeModeForNextProof) { SlicingSettingsProvider.getSlicingSettings() diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index f8c408348fc..df796188f2d 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -165,14 +165,10 @@ public class SlicingLeftPanel extends JPanel implements TabPanel, KeYSelectionLi */ private int graphEdgesNr = 0; /** - * Indicates whether graph statistics ({@link #graphNodes}, {@link #graphEdges}) need to be - * updated based on {@link #graphNodesNr} and {@link #graphEdgesNr}. + * Timer to regularly update dependency graph statistics and other UI state when loading a + * proof. */ - private boolean updateGraphLabels = false; - /** - * Timer to regularly update dependency graph statistics when loading a proof. - */ - private Timer updateGraphLabelsTimer; + private Timer updateUiStateTimer; /** * Construct a new panel for this extension. @@ -194,11 +190,17 @@ public SlicingLeftPanel(KeYMediator mediator, SlicingExtension extension) { this.mediator = mediator; this.extension = extension; - updateGraphLabelsTimer = new Timer(100, e -> { - if (updateGraphLabels) { + updateUiStateTimer = new Timer(500, e -> { + var tracker = extension.trackers.get(currentProof); + if (tracker != null) { + graphNodesNr = tracker.getDependencyGraph().countNodes(); + graphEdgesNr = tracker.getDependencyGraph().countEdges(); displayGraphLabels(); - updateGraphLabelsTimer.stop(); + } else { + resetGraphLabels(); } + updateUIState(); + updateUiStateTimer.stop(); }); } @@ -552,22 +554,16 @@ public void selectedProofChanged(KeYSelectionEvent e) { /** * Notify the panel that a rule has been applied on the currently opened proof. * - * @param proof proof - * @param tracker dependency tracker of that proof + * @param proof currently opened proof */ - public void ruleAppliedOnProof(Proof proof, DependencyTracker tracker) { + public void ruleAppliedOnProof(Proof proof) { currentProof = proof; - graphNodesNr = tracker.getDependencyGraph().countNodes(); - graphEdgesNr = tracker.getDependencyGraph().countEdges(); - updateGraphLabels = true; - updateGraphLabelsTimer.start(); - - updateUIState(); + updateUiStateTimer.start(); } @Override public void proofPruned(ProofTreeEvent e) { - ruleAppliedOnProof(e.getSource(), extension.trackers.get(e.getSource())); + ruleAppliedOnProof(e.getSource()); } private void updateUIState() {