Merge remote-tracking branch 'origin/main' into toolbarCleanup

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

@@ -7,15 +7,14 @@
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 
-/*
- * Is this a legacy option? Finding instantiations seems to be done by the prover, even if this
- * option is disabled. (Kai Wallisch, December 2013)
+/**
+ * Option to specify all instantiations manually (does not apply to the automatic solver).
  */
 public class MinimizeInteraction extends KeYMenuCheckBox {
     public static final String NAME = "Minimize Interaction";
     public static final String TOOL_TIP =
-        "If ticked and automated strategy (play button) is used, the prover tries to minimize user interaction, "
-            + "e.g., if the prover can find instantiations by itself, it will not ask the user to provide them.";
+        "If not ticked, applying a taclet manually will require you to instantiate " +
+            "all schema variables.";
 
     /**
      *

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

@@ -32,7 +32,7 @@ public SettingsDialog(MainWindow owner) {
         setTitle("Settings");
 
         mainWindow = owner;
-        ui = new SettingsUi(owner);
+        ui = new SettingsUi(owner, this);
 
         JPanel root = new JPanel(new BorderLayout());
         root.add(ui);
@@ -43,7 +43,7 @@ public SettingsDialog(MainWindow owner) {
         getRootPane().registerKeyboardAction(e -> dispose(),
             KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_IN_FOCUSED_WINDOW);
 
-        setSize(600, 400);
+        setSize(new Dimension(900, 600));
     }
 
     private JPanel createButtonBar() {
@@ -59,7 +59,8 @@ private JPanel createButtonBar() {
 
     public void setSettingsProvider(List<SettingsProvider> providers) {
         this.providers = providers;
-        this.ui.setSettingsProvider(providers);
+        int width = this.ui.setSettingsProvider(providers);
+        setSize(new Dimension(width, 600));
     }
 
     SettingsUi getUi() {

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

@@ -120,7 +120,6 @@ private SettingsDialog createDialog(MainWindow mainWindow) {
         dialog.setSettingsProvider(settingsProviders);
         dialog.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE);
         dialog.setIconImage(IconFactory.keyLogo());
-        dialog.setSize(800, 600);
         dialog.setLocationRelativeTo(mainWindow);
         return dialog;
     }

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

@@ -32,8 +32,20 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
     private static final long serialVersionUID = 3465371513326517504L;
 
     protected SettingsPanel() {
-        pCenter.setLayout(new MigLayout(new LC().fillX().wrapAfter(3), new AC().count(3).fill(1)
-                .grow(1000f, 1).size("16px", 2).grow(0f, 0).align("right", 0)));
+        pCenter.setLayout(new MigLayout(
+            // set up rows:
+            new LC().fillX()
+                    // remove the padding after the help icon
+                    .insets(null, null, null, "0").wrapAfter(3),
+            // set up columns:
+            new AC().count(3).fill(1)
+                    // label column does not grow
+                    .grow(0f, 0)
+                    // input area does grow
+                    .grow(1000f, 1)
+                    // help icon always has the same size
+                    .size("16px", 2)
+                    .align("right", 0)));
     }
 
     /**
@@ -215,6 +227,13 @@ protected JTextArea addTextArea(String title, String text, String info,
         return (JTextArea) field.getViewport().getView();
     }
 
+    protected JTextArea addTextAreaWithoutScroll(String title, String text, String info,
+            final Validator<String> validator) {
+        JTextArea field = createTextAreaWithoutScroll(text, validator);
+        addTitledComponent(title, field, info);
+        return field;
+    }
+
 
     /**
      * @param title

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

@@ -3,6 +3,7 @@
 import java.awt.*;
 import java.awt.event.KeyAdapter;
 import java.awt.event.KeyEvent;
+import java.util.ArrayList;
 import java.util.Collections;
 import java.util.Enumeration;
 import java.util.LinkedList;
@@ -15,25 +16,25 @@
 import javax.swing.tree.TreePath;
 
 import de.uka.ilkd.key.gui.MainWindow;
-import de.uka.ilkd.key.gui.fonticons.IconFactory;
 
 /**
  * @author Alexander Weigl
  * @version 1 (08.04.19)
  */
 public class SettingsUi extends JPanel {
     private static final long serialVersionUID = -217841876110516940L;
-    private static final Icon ICON_TREE_NODE_RETRACTED = IconFactory.TREE_NODE_EXPANDED.get();
-    private static final Icon ICON_TREE_NODE_EXPANDED = IconFactory.TREE_NODE_RETRACTED.get();
+    private static int calculatedWidth = 0;
 
     private final JSplitPane root;
+    private final JComponent westPanel;
     private DefaultTreeModel treeModel = new DefaultTreeModel(null, false);
     private final JTree treeSettingsPanels = new JTree(treeModel);
     private final JTextField txtSearch = new JTextField();
     private final MainWindow mainWindow;
-    // private JScrollPane center;
+    private final JDialog frame;
 
-    public SettingsUi(MainWindow mainWindow) {
+    public SettingsUi(MainWindow mainWindow, JDialog frame) {
+        this.frame = frame;
         this.mainWindow = mainWindow;
         treeSettingsPanels.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5));
         treeSettingsPanels.setCellRenderer(new DefaultTreeCellRenderer() {
@@ -46,16 +47,16 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean
                 SettingsProvider panel = node.provider;
                 JLabel lbl;
                 if (panel == null) {
-                    lbl = (JLabel) super.getTreeCellRendererComponent(tree, value, sel, expanded,
-                        leaf, row, hasFocus);
+                    // root entry
+                    lbl = (JLabel) super.getTreeCellRendererComponent(tree, "KeY Settings", sel,
+                        expanded, leaf, row, hasFocus);
+                    lbl.setFont(lbl.getFont().deriveFont(16f));
                 } else {
                     lbl = (JLabel) super.getTreeCellRendererComponent(tree, panel.getDescription(),
                         sel, expanded, leaf, row, hasFocus);
                     lbl.setFont(lbl.getFont().deriveFont(16f));
 
-                    if (!node.isLeaf()) {
-                        lbl.setIcon(expanded ? ICON_TREE_NODE_EXPANDED : ICON_TREE_NODE_RETRACTED);
-                    } else {
+                    if (node.isLeaf()) {
                         lbl.setIcon(panel.getIcon());
                     }
                     lbl.setBorder(BorderFactory.createEmptyBorder(2, 2, 2, 2));
@@ -94,20 +95,19 @@ public void keyReleased(KeyEvent e) {
             }
         });
 
-        treeSettingsPanels.setRootVisible(false);
         setLayout(new BorderLayout(5, 5));
-        root.setLeftComponent(createWestPanel());
+        westPanel = createWestPanel();
+        root.setLeftComponent(westPanel);
         root.setRightComponent(new JLabel("empty"));
         add(root, BorderLayout.CENTER);
         root.setDividerLocation(0.3d);
     }
 
     private void setSettingsPanel(JComponent comp) {
-        // int dividerLocation = root.getDividerLocation();
         root.setRightComponent(comp);
-        // root.setDividerLocation(dividerLocation);
 
-        root.setDividerLocation(root.getLeftComponent().getPreferredSize().width);
+        // set divider location slightly more to the right to avoid horizontal scroll bar
+        root.setDividerLocation(root.getLeftComponent().getPreferredSize().width + 2);
     }
 
     private JPanel createWestPanel() {
@@ -123,7 +123,13 @@ private JPanel createWestPanel() {
         return p;
     }
 
-    public void setSettingsProvider(List<SettingsProvider> providers) {
+    /**
+     * Configure the settings providers to display. Calculates the maximum width of the settings UI.
+     *
+     * @param providers settings providers
+     * @return maximum width of the dialog
+     */
+    public int setSettingsProvider(List<SettingsProvider> providers) {
         SettingsTreeNode root = new SettingsTreeNode(providers);
         treeModel = new DefaultTreeModel(root);
         treeSettingsPanels.setModel(treeModel);
@@ -134,15 +140,41 @@ public void setSettingsProvider(List<SettingsProvider> providers) {
         if (!providers.isEmpty()) {
             setSettingsPanel(providers.get(0).getPanel(mainWindow));
         }
+        // determine optimal dialog width
+        if (calculatedWidth != 0) {
+            return calculatedWidth;
+        }
+        int w = providers.stream().flatMap(x -> {
+            // collect all children providers
+            List<SettingsProvider> all = new ArrayList<>();
+            List<SettingsProvider> q = List.of(x);
+            while (!q.isEmpty()) {
+                List<SettingsProvider> newQ = new ArrayList<>();
+                for (var provider : q) {
+                    all.add(provider);
+                    newQ.addAll(provider.getChildren());
+                }
+                q = newQ;
+            }
+            return all.stream();
+        }).map(x -> {
+            JPanel panel = (JPanel) x.getPanel(mainWindow);
+            setSettingsPanel(panel);
+            frame.pack();
+            return panel.getWidth();
+        }).max(Integer::compareTo).orElse(600);
+        setSettingsPanel(!providers.isEmpty() ? providers.get(0).getPanel(mainWindow) : null);
+        calculatedWidth = w + westPanel.getWidth() + this.root.getDividerSize() + 30;
+        return calculatedWidth;
     }
 
     public void getPaths(TreePath parent, List<TreePath> list) {
         list.add(parent);
 
         TreeNode node = (TreeNode) parent.getLastPathComponent();
         if (node.getChildCount() >= 0) {
-            for (Enumeration e = node.children(); e.hasMoreElements();) {
-                TreeNode n = (TreeNode) e.nextElement();
+            for (Enumeration<? extends TreeNode> e = node.children(); e.hasMoreElements();) {
+                TreeNode n = e.nextElement();
                 TreePath path = parent.pathByAddingChild(n);
                 getPaths(path, list);
             }

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

@@ -108,6 +108,13 @@ protected JScrollPane createTextArea(String text, Validator<String> validator) {
         return new JScrollPane(area);
     }
 
+    protected JTextArea createTextAreaWithoutScroll(String text, Validator<String> validator) {
+        JTextArea area = new JTextArea(text);
+        area.setRows(5);
+        area.getDocument().addDocumentListener(new DocumentValidatorAdapter(area, validator));
+        return area;
+    }
+
 
     protected JTextField createTextField(String text, final @Nullable Validator<String> validator) {
         JTextField field = new JTextField(text);

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

@@ -6,6 +6,7 @@
 import javax.swing.*;
 
 import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.actions.MinimizeInteraction;
 import de.uka.ilkd.key.gui.configuration.Config;
 import de.uka.ilkd.key.settings.GeneralSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
@@ -107,7 +108,8 @@ public StandardUISettings() {
         chkConfirmExit = addCheckBox("Confirm program exit", "", false, emptyValidator());
         spAutoSaveProof =
             addNumberField("Auto save proof", 0, 10000000, 1000, "", emptyValidator());
-        chkMinimizeInteraction = addCheckBox("Minimise interactions", "", false, emptyValidator());
+        chkMinimizeInteraction = addCheckBox("Minimise interactions", MinimizeInteraction.TOOL_TIP,
+            false, emptyValidator());
         chkEnsureSourceConsistency =
             addCheckBox("Ensure source consistency", "", true, emptyValidator());
         chkRightClickMacros =

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

@@ -54,7 +54,7 @@ public SolverOptions(SolverType solverType) {
         createCheckSupportButton();
     }
 
-    private static final String versionInfo(String info, String versionString) {
+    private static String versionInfo(String info, String versionString) {
         String builder = info +
             " " +
             "(" +
@@ -85,12 +85,21 @@ private String getSolverSupportText() {
         }
     }
 
-    private JTextField createSolverInformation() {
+    private JTextArea createSolverInformation() {
         String info = solverType.getInfo();
         if (info != null && !info.equals("")) {
-            JTextField solverInfo =
-                addTextField("Info", info, BUNDLE.getString(INFO_SOLVER_INFO), null);
+            JTextArea solverInfo =
+                addTextAreaWithoutScroll("Info", info, BUNDLE.getString(INFO_SOLVER_INFO), null);
+            solverInfo.setLineWrap(true);
+            solverInfo.setWrapStyleWord(true);
             solverInfo.setEditable(false);
+
+            // text field to copy style from
+            JTextField textField = new JTextField();
+            textField.setEditable(false);
+            solverInfo.setBackground(textField.getBackground());
+            solverInfo.setBorder(textField.getBorder());
+
             return solverInfo;
         }
         return null;