Add new buttons to statistics dialog

KeYProject · Jul 10, 2023 · 7322c85 · 7322c85
1 parent ae3b90a
commit 7322c85
Show file tree

Hide file tree

Showing 6 changed files with 103 additions and 41 deletions.
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
@@ -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
@@ -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/...c/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java b/...c/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
@@ -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
@@ -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
@@ -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);
 }