Skip to content

Commit

Permalink
repairing heatmap updates for inner nodes (KeYProject#3506)
Browse files Browse the repository at this point in the history
  • Loading branch information
mattulbrich authored Aug 29, 2024
2 parents beffcf6 + 0d77d42 commit e20a4dd
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 18 deletions.
11 changes: 10 additions & 1 deletion key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
Original file line number Diff line number Diff line change
Expand Up @@ -1225,7 +1225,7 @@ private synchronized void updateSequentView() {
}

Runnable sequentUpdater = () -> {
mainFrame.setContent(newSequentView);
mainFrame.setSequentView(newSequentView);
// always does printSequent if on the event thread
sequentViewSearchBar.setSequentView(newSequentView);
};
Expand Down Expand Up @@ -1256,6 +1256,15 @@ public void scrollTo(int y) {
mainFrame.scrollTo(y);
}

/**
* Get the main frame for access to the sequent view
*
* @return the container for this main window.
*/
public MainFrame getMainFrame() {
return mainFrame;
}

void displayResults(String message) {
LOGGER.debug("displaying results: {}", message);
setStatusLine(message);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.gui.actions;

import java.awt.*;
import java.awt.event.ActionEvent;
import java.beans.PropertyChangeListener;
import javax.swing.*;
Expand All @@ -11,6 +12,7 @@
import de.uka.ilkd.key.core.KeYSelectionListener;
import de.uka.ilkd.key.gui.MainWindow;
import de.uka.ilkd.key.gui.fonticons.IconFactory;
import de.uka.ilkd.key.gui.nodeviews.SequentView;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
import de.uka.ilkd.key.settings.ViewSettings;
Expand Down Expand Up @@ -65,7 +67,10 @@ public void actionPerformed(ActionEvent e) {
vs.setHeatmapOptions(!vs.isShowHeatmap(), vs.isHeatmapSF(), vs.isHeatmapNewest(),
vs.getMaxAgeForHeatmap());
// this updates the heatmap highlights
mainWindow.getCurrentGoalView().getHighlighter().removeAllHighlights();
mainWindow.getCurrentGoalView().printSequent();
SequentView sequentView = mainWindow.getMainFrame().getSequentView();
if (sequentView != null) {
sequentView.getHighlighter().removeAllHighlights();
sequentView.printSequent();
}
}
}
33 changes: 18 additions & 15 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java
Original file line number Diff line number Diff line change
Expand Up @@ -26,27 +26,26 @@ public final class MainFrame extends JPanel {
private static final long serialVersionUID = -2412537422601138379L;

private final JScrollPane scrollPane = new JScrollPane();
private Component content;
private SequentView sequentView;
private boolean showTacletInfo = false;

public Component setContent(Component component) {
Component oldContent = content;
content = component;
if (component instanceof SequentView sequentView) {
public void setSequentView(SequentView component) {
SequentView oldSequentView = sequentView;
sequentView = component;
if (component != null) {
Point oldSequentViewPosition = scrollPane.getViewport().getViewPosition();
scrollPane.setViewportView(new SequentViewPanel(sequentView));
scrollPane.setViewportView(new SequentViewPanel(component));
scrollPane.getViewport().setViewPosition(oldSequentViewPosition);

setShowTacletInfo(showTacletInfo);
} else {
scrollPane.setViewportView(component);
}

if (oldContent instanceof SequentView) {
((SequentView) oldContent).removeUserSelectionHighlight();
if (oldSequentView != null) {
oldSequentView.removeUserSelectionHighlight();
}

return oldContent;
}

public MainFrame(final MainWindow mainWindow, EmptySequent emptySequent) {
Expand All @@ -58,8 +57,8 @@ public MainFrame(final MainWindow mainWindow, EmptySequent emptySequent) {

@Override
public void mouseClicked(MouseEvent e) {
if (content != null) {
for (MouseListener listener : content.getMouseListeners()) {
if (sequentView != null) {
for (MouseListener listener : sequentView.getMouseListeners()) {
if (listener instanceof SequentViewInputListener) {
listener.mouseClicked(e);
}
Expand All @@ -72,8 +71,8 @@ public void mouseClicked(MouseEvent e) {

@Override
public void ancestorRemoved(AncestorEvent event) {
if (content instanceof SequentView) {
((SequentView) content).removeUserSelectionHighlight();
if (sequentView != null) {
sequentView.removeUserSelectionHighlight();
}
}

Expand All @@ -90,13 +89,13 @@ public void ancestorAdded(AncestorEvent event) {}
getActionMap().put("copy", new CopyToClipboardAction(mainWindow));
setLayout(new BorderLayout());
add(scrollPane);
setContent(emptySequent);
setSequentView(emptySequent);
}

public void setShowTacletInfo(boolean showTacletInfo) {
this.showTacletInfo = showTacletInfo;

if (content instanceof InnerNodeView view) {
if (sequentView instanceof InnerNodeView view) {
view.tacletInfo.setVisible(this.showTacletInfo);
}
}
Expand All @@ -113,4 +112,8 @@ public boolean isShowTacletInfo() {
public void scrollTo(int y) {
scrollPane.getVerticalScrollBar().setValue(y);
}

public SequentView getSequentView() {
return sequentView;
}
}

0 comments on commit e20a4dd

Please sign in to comment.