diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java index 2fe4d3c1761..1146a794958 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java @@ -23,6 +23,8 @@ import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; +import de.uka.ilkd.key.gui.plugins.caching.DefaultReferenceSearchDialogListener; +import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearchDialog; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Statistics; @@ -282,6 +284,7 @@ private void init(MainWindow mainWindow, String stats) { } JPanel buttonPane = new JPanel(); + JPanel buttonPane2 = new JPanel(); JButton okButton = new JButton("Close"); okButton.addActionListener(event -> dispose()); @@ -296,9 +299,33 @@ private void init(MainWindow mainWindow, String stats) { event -> export("html", MiscTools.toValidFileName(proof.name().toString()), ShowProofStatistics.getHTMLStatisticsMessage(proof))); + JButton saveButton = new JButton("Save proof"); + saveButton.addActionListener( + e -> mainWindow.getUserInterface().saveProof(proof, ".proof")); + JButton saveBundleButton = new JButton("Save proof bundle"); + saveBundleButton + .addActionListener(e -> mainWindow.getUserInterface().saveProofBundle(proof)); + buttonPane.add(okButton); buttonPane.add(csvButton); buttonPane.add(htmlButton); + buttonPane2.add(saveButton); + buttonPane2.add(saveBundleButton); + + if (proof.openGoals().stream().anyMatch(g -> g.node().lookup(ClosedBy.class) != null)) { + JButton copyReferences = new JButton("Copy referenced proof"); + copyReferences.addActionListener(e -> { + dispose(); + ReferenceSearchDialog dialog = + new ReferenceSearchDialog(proof, new DefaultReferenceSearchDialogListener( + MainWindow.getInstance().getMediator())); + // show the dialog and start the copy + // (two callbacks because setVisible will block) + SwingUtilities.invokeLater(() -> dialog.setVisible(true)); + SwingUtilities.invokeLater(dialog::apply); + }); + buttonPane2.add(copyReferences); + } getRootPane().setDefaultButton(okButton); getRootPane().addKeyListener(new KeyAdapter() { @@ -313,12 +340,18 @@ public void keyTyped(KeyEvent e) { setLayout(new BorderLayout()); add(scrollPane, BorderLayout.CENTER); - add(buttonPane, BorderLayout.PAGE_END); + JPanel buttonsPane = new JPanel(); + BoxLayout layout = new BoxLayout(buttonsPane, BoxLayout.Y_AXIS); + buttonsPane.setLayout(layout); + buttonsPane.add(Box.createVerticalGlue()); + buttonsPane.add(buttonPane); + buttonsPane.add(buttonPane2); + add(buttonsPane, BorderLayout.PAGE_END); int w = 50 + Math.max(scrollPane.getPreferredSize().width, - buttonPane.getPreferredSize().width); + buttonsPane.getPreferredSize().width); int h = - scrollPane.getPreferredSize().height + buttonPane.getPreferredSize().height + 100; + scrollPane.getPreferredSize().height + buttonsPane.getPreferredSize().height + 100; setSize(w, h); setLocationRelativeTo(mainWindow); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingDatabase.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingDatabase.java index b324e5b2b4d..009bd161a34 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingDatabase.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingDatabase.java @@ -92,7 +92,8 @@ public static void init() { var entry = files.item(i); var name = entry.getAttributes().getNamedItem("name").getNodeValue(); var hash = entry.getAttributes().getNamedItem("hash").getNodeValue(); - CachingDatabase.files.put(Integer.parseInt(hash), new CachedFile(name, Integer.parseInt(hash))); + CachingDatabase.files.put(Integer.parseInt(hash), + new CachedFile(name, Integer.parseInt(hash))); } } catch (Exception e) { LOGGER.error("failed to load proof caching database ", e); @@ -244,7 +245,10 @@ public static void addProof(Proof proof) throws IOException { Files.createLink(virtualSource.resolve(path.filename), PathConfig.getCacheDirectory().toPath().resolve(path.filename)); } - // TODO: bootstrap path etc. + // TODO: bootstrap path (save hash) + // TODO: modify existing proof header + // TODO: save includes recursively + // TODO: save proofs compressed // construct new header var proofHeader = new StringBuilder(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java new file mode 100644 index 00000000000..006231cb81a --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java @@ -0,0 +1,49 @@ +package de.uka.ilkd.key.gui.plugins.caching; + +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.ShowProofStatistics; +import de.uka.ilkd.key.proof.Proof; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +public class DefaultReferenceSearchDialogListener implements ReferenceSearchDialogListener { + private static final Logger LOGGER = + LoggerFactory.getLogger(DefaultReferenceSearchDialogListener.class); + private final KeYMediator mediator; + + public DefaultReferenceSearchDialogListener(KeYMediator mediator) { + this.mediator = mediator; + } + + @Override + public void closeButtonClicked(ReferenceSearchDialog dialog) { + dialog.dispose(); + } + + @Override + public void copyButtonClicked(ReferenceSearchDialog dialog) { + System.out.println("copy clicked !!!"); + mediator.stopInterface(true); + Proof p = mediator.getSelectedProof(); + new Thread(() -> { + try { + p.copyCachedGoals(null, + total -> SwingUtilities.invokeLater(() -> dialog.setMaximum(total)), + () -> SwingUtilities.invokeLater(() -> { + if (dialog.incrementProgress()) { + mediator.startInterface(true); + dialog.dispose(); + new ShowProofStatistics.Window(MainWindow.getInstance(), p) + .setVisible(true); + } + })); + } catch (Exception e) { + LOGGER.error("failed to copy cache ", e); + } + }).start(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index 33faebfc6fb..6fcbaf75541 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -8,8 +8,6 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.actions.ShowProofStatistics; import de.uka.ilkd.key.gui.colors.ColorSettings; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -21,8 +19,7 @@ * * @author Arne Keller */ -public class ReferenceSearchButton extends JButton - implements ActionListener, ReferenceSearchDialogListener, KeYSelectionListener { +public class ReferenceSearchButton extends JButton implements ActionListener, KeYSelectionListener { /** * Color used for the label if a reference is found. */ @@ -69,37 +66,10 @@ public void actionPerformed(ActionEvent e) { mediator, c.getProof(), p)); } } - dialog = new ReferenceSearchDialog(p, this); + dialog = new ReferenceSearchDialog(p, new DefaultReferenceSearchDialogListener(mediator)); dialog.setVisible(true); } - @Override - public void closeButtonClicked() { - if (dialog != null) { - dialog.dispose(); - dialog = null; - } - } - - @Override - public void copyButtonClicked() { - if (dialog != null) { - mediator.stopInterface(true); - Proof p = mediator.getSelectedProof(); - new Thread(() -> p.copyCachedGoals(null, - total -> SwingUtilities.invokeLater(() -> dialog.setMaximum(total)), - () -> SwingUtilities.invokeLater(() -> { - if (dialog.incrementProgress()) { - mediator.startInterface(true); - dialog.dispose(); - dialog = null; - new ShowProofStatistics.Window(MainWindow.getInstance(), p) - .setVisible(true); - } - }))).start(); - } - } - @Override public void selectedNodeChanged(KeYSelectionEvent e) { Proof p = e.getSource().getSelectedProof(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java index 00f459b4449..b2dce4fe13f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java @@ -100,7 +100,9 @@ private JButton getApplyButton() { applyButton.setEnabled(false); applyButton.addActionListener(e -> { try { - listener.copyButtonClicked(); + applyButton.setEnabled(false); + closeDialog.setEnabled(false); + listener.copyButtonClicked(this); } catch (Exception exception) { // There may be exceptions during rule application that should not be lost. IssueDialog.showExceptionDialog(ReferenceSearchDialog.this, exception); @@ -110,6 +112,10 @@ private JButton getApplyButton() { return applyButton; } + public void apply() { + getApplyButton().doClick(); + } + private JScrollPane getScrollPane() { if (scrollPane == null) { scrollPane = new JScrollPane(table, ScrollPaneConstants.VERTICAL_SCROLLBAR_ALWAYS, @@ -127,7 +133,7 @@ private JScrollPane getScrollPane() { private JButton getCloseDialog() { if (closeDialog == null) { closeDialog = new JButton("Close"); - closeDialog.addActionListener(e -> listener.closeButtonClicked()); + closeDialog.addActionListener(e -> listener.closeButtonClicked(this)); } return closeDialog; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java index 7b2bd812af8..18f9bf20136 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java @@ -9,10 +9,10 @@ public interface ReferenceSearchDialogListener { /** * Button to close the dialog has been activated. */ - void closeButtonClicked(); + void closeButtonClicked(ReferenceSearchDialog dialog); /** * Button to copy proof steps has been activated. */ - void copyButtonClicked(); + void copyButtonClicked(ReferenceSearchDialog dialog); }