Skip to content

Commit

Permalink
Make settings dialog look nicer (#3179)
Browse files Browse the repository at this point in the history
Changes done:
- automatic width calculation based on largest settings panel
- less padding next to the help icon
- fix for #1645

Feel free to comment on the new look:

![image](https://github.com/KeYProject/key/assets/12560461/6bfcb637-73f2-4f7e-9d2d-d541155f2381)
  • Loading branch information
WolframPfeifer authored Jul 12, 2023
2 parents fc867d3 + 339d573 commit f798501
Show file tree
Hide file tree
Showing 8 changed files with 102 additions and 34 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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.";

/**
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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() {
Expand All @@ -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() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
}

/**
Expand Down Expand Up @@ -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
Expand Down
68 changes: 50 additions & 18 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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() {
Expand All @@ -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));
Expand Down Expand Up @@ -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() {
Expand All @@ -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);
Expand All @@ -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);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 +
" " +
"(" +
Expand Down Expand Up @@ -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;
Expand Down

0 comments on commit f798501

Please sign in to comment.