From 79ce908e75370f3b7c59ebf0b6e7e1b92d3afcd8 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 22 Jun 2023 19:00:22 +0200 Subject: [PATCH 1/9] Make settings dialog look nicer --- .../java/de/uka/ilkd/key/gui/settings/SettingsUi.java | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index d811099fb78..4e9f921e9f4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -46,16 +46,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,7 +94,6 @@ public void keyReleased(KeyEvent e) { } }); - treeSettingsPanels.setRootVisible(false); setLayout(new BorderLayout(5, 5)); root.setLeftComponent(createWestPanel()); root.setRightComponent(new JLabel("empty")); From e115f1ffba34a463be676f53987d4e3f2243d293 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 23 Jun 2023 19:36:53 +0200 Subject: [PATCH 2/9] Increase default size of settings dialog --- .../main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java | 2 +- .../main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index 782e239c548..ee773f5fef5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java @@ -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() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index 7b536fa28a3..7fb499cb254 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/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.setLocationByPlatform(true); return dialog; } From 71263b2161e3dbce49c8f739490cd0d00b3ad692 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 29 Jun 2023 15:17:12 +0200 Subject: [PATCH 3/9] Avoid scroll bar in settings tree --- .../main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index 4e9f921e9f4..f8242b5c51b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -102,11 +102,10 @@ public void keyReleased(KeyEvent e) { } 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() { From 00e2dceb1de293a4ef12c30c95b25c8031e19e51 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 29 Jun 2023 15:27:07 +0200 Subject: [PATCH 4/9] Automatically set width --- .../ilkd/key/gui/settings/SettingsDialog.java | 5 ++-- .../uka/ilkd/key/gui/settings/SettingsUi.java | 23 +++++++++++++------ 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index ee773f5fef5..5cc0a631498 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/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); @@ -59,7 +59,8 @@ private JPanel createButtonBar() { public void setSettingsProvider(List providers) { this.providers = providers; - this.ui.setSettingsProvider(providers); + int width = this.ui.setSettingsProvider(providers); + setSize(new Dimension(width, 600)); } SettingsUi getUi() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index f8242b5c51b..2b19d315185 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -15,7 +15,6 @@ import javax.swing.tree.TreePath; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.fonticons.IconFactory; /** * @author Alexander Weigl @@ -23,17 +22,17 @@ */ 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 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() { @@ -95,7 +94,8 @@ public void keyReleased(KeyEvent e) { }); 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); @@ -121,7 +121,7 @@ private JPanel createWestPanel() { return p; } - public void setSettingsProvider(List providers) { + public int setSettingsProvider(List providers) { SettingsTreeNode root = new SettingsTreeNode(providers); treeModel = new DefaultTreeModel(root); treeSettingsPanels.setModel(treeModel); @@ -132,6 +132,15 @@ public void setSettingsProvider(List providers) { if (!providers.isEmpty()) { setSettingsPanel(providers.get(0).getPanel(mainWindow)); } + // determine optimal dialog width + int w = providers.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); + return w + westPanel.getWidth() + 15; } public void getPaths(TreePath parent, List list) { From fe3818851b2d96acb4cf01198195b3169fc4a1e5 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 3 Jul 2023 08:03:16 +0200 Subject: [PATCH 5/9] Remove some padding in the settings --- .../uka/ilkd/key/gui/settings/SettingsPanel.java | 16 ++++++++++++++-- .../de/uka/ilkd/key/gui/settings/SettingsUi.java | 6 ++++++ 2 files changed, 20 insertions(+), 2 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index c9ccaaabd7c..707c5a1c42b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/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))); } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index 2b19d315185..dcdf3d56750 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -121,6 +121,12 @@ private JPanel createWestPanel() { return p; } + /** + * 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 providers) { SettingsTreeNode root = new SettingsTreeNode(providers); treeModel = new DefaultTreeModel(root); From c59434dbed553432f7c368024914b3a70c49f25f Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 3 Jul 2023 08:24:49 +0200 Subject: [PATCH 6/9] Also check children settings providers --- .../de/uka/ilkd/key/gui/settings/SettingsUi.java | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index dcdf3d56750..f203a2ad81a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/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; @@ -139,7 +140,20 @@ public int setSettingsProvider(List providers) { setSettingsPanel(providers.get(0).getPanel(mainWindow)); } // determine optimal dialog width - int w = providers.stream().map(x -> { + int w = providers.stream().flatMap(x -> { + // collect all children providers + List all = new ArrayList<>(); + List q = List.of(x); + while (!q.isEmpty()) { + List 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(); From 3171c8da02442804b20c6b20f9a0ace855126f92 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 11 Jul 2023 07:56:17 +0200 Subject: [PATCH 7/9] Consider divider width in layout --- .../java/de/uka/ilkd/key/gui/settings/SettingsUi.java | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java index f203a2ad81a..6d1532e8be9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java @@ -23,6 +23,7 @@ */ public class SettingsUi extends JPanel { private static final long serialVersionUID = -217841876110516940L; + private static int calculatedWidth = 0; private final JSplitPane root; private final JComponent westPanel; @@ -140,6 +141,9 @@ public int setSettingsProvider(List providers) { 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 all = new ArrayList<>(); @@ -160,7 +164,8 @@ public int setSettingsProvider(List providers) { return panel.getWidth(); }).max(Integer::compareTo).orElse(600); setSettingsPanel(!providers.isEmpty() ? providers.get(0).getPanel(mainWindow) : null); - return w + westPanel.getWidth() + 15; + calculatedWidth = w + westPanel.getWidth() + this.root.getDividerSize() + 30; + return calculatedWidth; } public void getPaths(TreePath parent, List list) { @@ -168,8 +173,8 @@ public void getPaths(TreePath parent, List list) { TreeNode node = (TreeNode) parent.getLastPathComponent(); if (node.getChildCount() >= 0) { - for (Enumeration e = node.children(); e.hasMoreElements();) { - TreeNode n = (TreeNode) e.nextElement(); + for (Enumeration e = node.children(); e.hasMoreElements();) { + TreeNode n = e.nextElement(); TreePath path = parent.pathByAddingChild(n); getPaths(path, list); } From 0c1d442af9671c47a7eb818e230d9ea67a8e1363 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 11 Jul 2023 08:19:14 +0200 Subject: [PATCH 8/9] Show SMT solver info in text area --- .../ilkd/key/gui/settings/SettingsPanel.java | 7 +++++++ .../key/gui/settings/SimpleSettingsPanel.java | 7 +++++++ .../key/gui/smt/settings/SolverOptions.java | 17 +++++++++++++---- 3 files changed, 27 insertions(+), 4 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index 707c5a1c42b..9ed74bf8288 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -227,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 validator) { + JTextArea field = createTextAreaWithoutScroll(text, validator); + addTitledComponent(title, field, info); + return field; + } + /** * @param title diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java index 4973ac1d19f..37d328b4088 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java @@ -108,6 +108,13 @@ protected JScrollPane createTextArea(String text, Validator validator) { return new JScrollPane(area); } + protected JTextArea createTextAreaWithoutScroll(String text, Validator 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 validator) { JTextField field = new JTextField(text); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java index a35e13e1a8d..f15d9823787 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java +++ b/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; From 339d573bc3ff129efe520addab231f3670cd688b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 11 Jul 2023 08:32:07 +0200 Subject: [PATCH 9/9] Document 'minimize interactions' correctly --- .../de/uka/ilkd/key/gui/actions/MinimizeInteraction.java | 9 ++++----- .../de/uka/ilkd/key/gui/settings/StandardUISettings.java | 4 +++- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java index 0e01a646914..8a73cd295f8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java +++ b/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."; /** * diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java index 2b33ce013de..669ddc06f70 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java +++ b/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 =