HacKeYthon: Improved Taclet Options (#3433)

build.gradle

@@ -334,6 +334,8 @@ subprojects {
             targetExclude 'build/**'
 
             // allows us to use spotless:off / spotless:on to keep pre-formatted sections
+            // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on"
+            // that must be used instead.
             toggleOffOn()
 
             removeUnusedImports()

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -156,7 +156,8 @@ public Configuration asConfiguration() {
             if (!res.isEmpty())
                 return (Configuration) res.get(0);
             else
-                throw new RuntimeException();
+                throw new RuntimeException("Error in configuration. Source: "
+                    + ctx.start.getTokenSource().getSourceName());
         }
     }
 

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -1015,7 +1015,9 @@ public void menuCanceled(MenuEvent e) {
         }
         proof.addSeparator();
         proof.add(new ShowUsedContractsAction(this, selected));
-        proof.add(new ShowActiveTactletOptionsAction(this, selected));
+        // We merge the old window to view the active taclet options with the window for all active
+        // settings
+        // proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction));
         proof.add(showActiveSettingsAction);
         proof.add(new ShowProofStatistics(this, selected));
         proof.add(new ShowKnownTypesAction(this, selected));
@@ -1027,7 +1029,8 @@ private JMenu createOptionsMenu() {
         options.setMnemonic(KeyEvent.VK_O);
 
         options.add(SettingsManager.getActionShowSettings(this));
-        options.add(new TacletOptionsAction(this));
+        // remove since taclet options should only be set through the general settings dialog
+        // options.add(new TacletOptionsAction(this));
         options.add(new SMTOptionsAction(this));
         // options.add(setupSpeclangMenu()); // legacy since only JML supported
         options.addSeparator();
@@ -1038,7 +1041,6 @@ private JMenu createOptionsMenu() {
         options.add(new JCheckBoxMenuItem(new EnsureSourceConsistencyToggleAction(this)));
 
         return options;
-
     }
 
     private JMenu createHelpMenu() {

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java

@@ -3,12 +3,10 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.gui.actions;
 
+import java.util.Arrays;
 import java.util.Map.Entry;
 import java.util.Properties;
-import javax.swing.JComponent;
-import javax.swing.JScrollPane;
-import javax.swing.JTable;
-import javax.swing.JTextArea;
+import javax.swing.*;
 import javax.swing.table.DefaultTableModel;
 import javax.swing.tree.DefaultMutableTreeNode;
 import javax.swing.tree.DefaultTreeModel;
@@ -34,6 +32,7 @@ public class SettingsTreeModel extends DefaultTreeModel {
     private final ProofSettings proofSettings;
 
     private final ProofIndependentSettings independentSettings;
+    private OptionContentNode tacletOptionsItem;
 
     public SettingsTreeModel(ProofSettings proofSettings,
             ProofIndependentSettings independentSettings) {
@@ -46,19 +45,27 @@ public SettingsTreeModel(ProofSettings proofSettings,
     private void generateTree() {
         DefaultMutableTreeNode root = (DefaultMutableTreeNode) this.getRoot();
 
-        OptionContentNode proofSettingsNode =
-            generateOptionContentNode("Proof Settings", "These are the proof dependent settings.");
-        root.add(proofSettingsNode);
-
-        // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings();
-        ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-        proofSettingsNode.add(generateTableNode("Taclets", choiceSettings));
-
-        Settings strategySettings = proofSettings.getStrategySettings();
-        proofSettingsNode.add(generateTableNode("Strategy", strategySettings));
-
-        Settings smtSettings = proofSettings.getSMTSettings();
-        proofSettingsNode.add(generateTableNode("SMT", smtSettings));
+        if (proofSettings == null) {
+            OptionContentNode proofSettingsNode =
+                generateOptionContentNode("Proof Settings", "There is currently no proof loaded!");
+            root.add(proofSettingsNode);
+        } else {
+            OptionContentNode proofSettingsNode =
+                generateOptionContentNode("Proof Settings",
+                    "These are the proof dependent settings.");
+            root.add(proofSettingsNode);
+
+            // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings();
+            ChoiceSettings choiceSettings = proofSettings.getChoiceSettings();
+            tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings);
+            proofSettingsNode.add(tacletOptionsItem);
+
+            Settings strategySettings = proofSettings.getStrategySettings();
+            proofSettingsNode.add(generateTableNode("Strategy", strategySettings));
+
+            Settings smtSettings = proofSettings.getSMTSettings();
+            proofSettingsNode.add(generateTableNode("SMT", smtSettings));
+        }
 
         OptionContentNode independentSettingsNode = generateOptionContentNode(
             "Proof-Independent Settings", "These are the proof independent settings.");
@@ -75,7 +82,10 @@ private void generateTree() {
         Settings viewSettings = independentSettings.getViewSettings();
         independentSettingsNode.add(generateTableNode("View", viewSettings));
         Settings termLabelSettings = independentSettings.getTermLabelSettings();
-        proofSettingsNode.add(generateTableNode("Term Labels", termLabelSettings));
+        // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the
+        // previous line,
+        // it should really be added to the independentSettingsNode
+        independentSettingsNode.add(generateTableNode("Term Labels", termLabelSettings));
     }
 
 
@@ -115,6 +125,7 @@ private JComponent generateScrollPane(String text) {
         JTextArea ta = new JTextArea(5, 20);
         ta.append(text);
         ta.setEditable(false);
+        ta.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
         JScrollPane scrollpane = new JScrollPane(ta);
         return scrollpane;
     }
@@ -130,6 +141,8 @@ private JComponent generateJTable(Properties properties) {
             i++;
         }
 
+        Arrays.sort(data, (a, b) -> a[0].toString().compareToIgnoreCase(b[0].toString()));
+
         JTable table = new JTable();
 
         DefaultTableModel tableModel = new DefaultTableModel() {
@@ -143,9 +156,8 @@ public boolean isCellEditable(int row, int column) {
         };
 
         tableModel.setDataVector(data, columnNames);
-
         table.setModel(tableModel);
-
+        table.setRowHeight(table.getRowHeight() + 10);
 
         JScrollPane scrollpane = new JScrollPane(table);
         return scrollpane;
@@ -157,6 +169,7 @@ private OptionContentNode generateOptionContentNode(String title, String text) {
         return new OptionContentNode(title, generateScrollPane(text));
     }
 
-
-
+    public OptionContentNode getTacletOptionsItem() {
+        return tacletOptionsItem;
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java

@@ -22,9 +22,6 @@
  */
 public class ShowActiveSettingsAction extends MainWindowAction {
 
-    /**
-     *
-     */
     private static final long serialVersionUID = -3038735283059371442L;
 
     public ShowActiveSettingsAction(MainWindow mainWindow) {
@@ -35,15 +32,27 @@ public ShowActiveSettingsAction(MainWindow mainWindow) {
 
     @Override
     public void actionPerformed(ActionEvent e) {
+        showDialog();
+    }
+
+    private ViewSettingsDialog showDialog() {
         ProofSettings settings =
-            (getMediator().getSelectedProof() == null) ? ProofSettings.DEFAULT_SETTINGS
+            (getMediator().getSelectedProof() == null) ? null
                     : getMediator().getSelectedProof().getSettings();
         SettingsTreeModel model =
             new SettingsTreeModel(settings, ProofIndependentSettings.DEFAULT_INSTANCE);
         ViewSettingsDialog dialog = new ViewSettingsDialog(model, model.getStartComponent());
         dialog.setTitle("All active settings");
         dialog.setLocationRelativeTo(mainWindow);
         dialog.setVisible(true);
+        return dialog;
+    }
+
+    public void showAndFocusTacletOptions() {
+        ViewSettingsDialog dialog = showDialog();
+        SettingsTreeModel model = (SettingsTreeModel) dialog.optionTree.getModel();
+        OptionContentNode item = model.getTacletOptionsItem();
+        dialog.getOptionTree().setSelectionPath(new TreePath(item.getPath()));
     }
 
     /**
@@ -57,31 +66,33 @@ private class ViewSettingsDialog extends JDialog {
 
         public ViewSettingsDialog(TreeModel model, JComponent startComponent) {
             super(mainWindow);
-            this.getContentPane().setLayout(new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
-            Box box = Box.createHorizontalBox();
-            box.add(getSplitPane());
-            this.getContentPane().add(box);
-            this.getContentPane().add(Box.createVerticalStrut(5));
-            box = Box.createHorizontalBox();
-            box.add(Box.createHorizontalStrut(5));
+            Container cp = this.getContentPane();
+            cp.setLayout(new BorderLayout());
+            cp.add(getSplitPane(), BorderLayout.CENTER);
+
             JButton okButton = new JButton("OK");
             okButton.addActionListener(e -> dispose());
             setDefaultCloseOperation(DISPOSE_ON_CLOSE);
-            box.add(okButton);
-            box.add(Box.createHorizontalStrut(5));
-            this.getContentPane().add(box);
+            JPanel buttons = new JPanel(new FlowLayout());
+            buttons.add(okButton);
+            cp.add(buttons, BorderLayout.SOUTH);
+
+            JLabel announce =
+                new JLabel("<html>This shows the active settings for the current proof.<br>" +
+                    "To change settings for future proofs, use Options > Show Settings.");
+            announce.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5));
+            cp.add(announce, BorderLayout.NORTH);
+
             this.getOptionTree().setModel(model);
             getSplitPane().setRightComponent(startComponent);
 
             this.getOptionTree().getParent().setMinimumSize(getOptionTree().getPreferredSize());
-            this.getContentPane().setPreferredSize(computePreferredSize(model));
+            cp.setPreferredSize(computePreferredSize(model));
             this.setDefaultCloseOperation(DISPOSE_ON_CLOSE);
             setIconImage(IconFactory.keyLogo());
             this.pack();
             this.setLocationRelativeTo(MainWindow.getInstance());
 
-
-
             getRootPane().registerKeyboardAction((e) -> dispose(),
                 KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_IN_FOCUSED_WINDOW);
             getRootPane().setDefaultButton(okButton);
@@ -127,15 +138,14 @@ private JTree getOptionTree() {
                         }
                     }
                 });
+                optionTree.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5));
             }
             return optionTree;
         }
 
         private JSplitPane getSplitPane() {
             if (splitPane == null) {
-
                 splitPane = new JSplitPane();
-                splitPane.setAlignmentX(LEFT_ALIGNMENT);
                 splitPane.setLeftComponent(new JScrollPane(getOptionTree()));
                 splitPane.setRightComponent(getOptionPanel());
                 // splitPane.setResizeWeight(0.2);

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java

@@ -4,60 +4,57 @@
 package de.uka.ilkd.key.gui.actions;
 
 import java.awt.event.ActionEvent;
-import javax.swing.JOptionPane;
-import javax.swing.JTextArea;
-import javax.swing.text.JTextComponent;
 
 import de.uka.ilkd.key.gui.MainWindow;
-import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent;
-import de.uka.ilkd.key.proof.Proof;
 
+/**
+ * Action to show a dialog with the taclet options valid for the currently
+ * selected proof.
+ *
+ * Now defers to the "Show Active Settings" action to show the taclet options.
+ */
 public class ShowActiveTactletOptionsAction extends MainWindowAction {
 
-    /**
-     *
-     */
     private static final long serialVersionUID = -7012564698194718532L;
+    private final ShowActiveSettingsAction action;
 
-    private final Proof proof;
-
-    public ShowActiveTactletOptionsAction(MainWindow mainWindow, Proof proof) {
+    public ShowActiveTactletOptionsAction(MainWindow mainWindow, ShowActiveSettingsAction action) {
         super(mainWindow);
         setName("Show Active Taclet Options");
-
-        getMediator().enableWhenProofLoaded(this);
-
-        this.proof = proof;
+        this.action = action;
     }
 
     @Override
     public void actionPerformed(ActionEvent e) {
-        showActivatedChoices();
+        action.showAndFocusTacletOptions();
     }
 
-    private void showActivatedChoices() {
-        Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof;
-        if (currentProof == null) {
-            mainWindow.notify(new GeneralInformationEvent("No Options available.",
-                "If you wish to see Taclet Options " + "for a proof you have to load one first"));
-        } else {
-            StringBuilder message = new StringBuilder("Active Taclet Options:\n");
-            int rows = 0;
-            int columns = 0;
-            for (final String choice : currentProof.getSettings().getChoiceSettings()
-                    .getDefaultChoices().values()) {
-                message.append(choice).append("\n");
-                rows++;
-                if (columns < choice.length()) {
-                    columns = choice.length();
-                }
-            }
-            final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns);
-            activeOptions.setEditable(false);
-            Object[] toDisplay =
-                { activeOptions, "These options can be changed in Options->Taclet Options" };
-            JOptionPane.showMessageDialog(mainWindow, toDisplay,
-                "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE);
-        }
-    }
+    // @formatter:off
+
+//    private void showActivatedChoices() {
+//        Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof;
+//        if (currentProof == null) {
+//            mainWindow.notify(new GeneralInformationEvent("No Options available.",
+//                "If you wish to see Taclet Options " + "for a proof you have to load one first"));
+//        } else {
+//            StringBuilder message = new StringBuilder("Active Taclet Options:\n");
+//            int rows = 0;
+//            int columns = 0;
+//            for (final String choice : currentProof.getSettings().getChoiceSettings()
+//                    .getDefaultChoices().values()) {
+//                message.append(choice).append("\n");
+//                rows++;
+//                if (columns < choice.length()) {
+//                    columns = choice.length();
+//                }
+//            }
+//            final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns);
+//            activeOptions.setEditable(false);
+//            Object[] toDisplay =
+//                { activeOptions,
+//                    "These options can be changed in Options->Show Settings->Taclet Options" };
+//            JOptionPane.showMessageDialog(mainWindow, toDisplay,
+//                "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE);
+//        }
+//    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java

@@ -11,6 +11,9 @@
 import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent;
 import de.uka.ilkd.key.settings.ProofSettings;
 
+// This class is not used anymore as taclet options should be set through the general settings
+// dialog
+@Deprecated
 public class TacletOptionsAction extends MainWindowAction {
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java

@@ -108,7 +108,8 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings {
         defineDefault(SaveBundleAction.class, KeyEvent.VK_B, SHORTCUT_KEY_MASK);
         defineDefault(SaveFileAction.class, KeyEvent.VK_S, SHORTCUT_KEY_MASK);
         defineDefault(SettingsManager.ShowSettingsAction.class, KeyEvent.VK_N, SHORTCUT_KEY_MASK);
-        defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK);
+        // remove as the old menu should not be accessible anymore
+        // defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK);
         defineDefault(OpenFileAction.class, KeyEvent.VK_O, SHORTCUT_KEY_MASK);
         defineDefault(SearchInSequentAction.class, KeyEvent.VK_F, SHORTCUT_KEY_MASK);
 

key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java

@@ -78,6 +78,7 @@ SettingsUi getUi() {
     private List<Exception> apply() {
         List<Exception> exc = new LinkedList<>();
         apply(providers, exc);
+
         return exc;
     }